Vortrag: Modeling Time in Java Programs for Automatic Error Detection
Stammdaten
Titel: | Modeling Time in Java Programs for Automatic Error Detection |
Beschreibung: | Modern programming languages, such as Java, represent time as integer variables, called timestamps. Timestamps allow developers to tacitly model incorrect time values resulting in a program failure because any negative value or every positive value is not necessarily a valid time representation. Current approaches to automatically detect errors in programs, such as Randoop and FindBugs, cannot detect such errors because they treat timestamps as normal integer variables and test them with random values verifying if the program throws an exception. In this paper, we present an approach that considers the time semantics of the Java language to systematically detect time related errors in Java programs. With the formal time semantics, our approach determines which integer variables handle time and which statements use or alter their values. Based on this information, it translates these statements into an SMT model that is passed to an SMT solver. The solver formally verifies the correctness of the model and reports the violations of time properties in that program. For the evaluation, we have implemented our approach in a prototype tool and applied it to the source code of 20 Java open source projects. The results show that our approach is scalable and it is capable of detecting time errors precisely enough allowing its usability in real-world applications. |
Schlagworte: |
Typ: | Angemeldeter Vortrag |
Homepage: | - |
Veranstaltung: | 6th Conference on Formal Methods in Software Engineering (Gothenburg) |
Datum: | 02.06.2018 |
Vortragsstatus: |
Beteiligte
Giovanni Liva (intern) |
|
||||
Muhammad Taimoor Khan (intern) |
|
||||
Francesco Spegni
|
|
||||
Luca Spalazzi
|
|
||||
Andreas Bollin (intern) |
|
||||
Martin Pinzger (intern) |
|
Zuordnung
Organisation | Adresse | ||||
---|---|---|---|---|---|
Fakultät für Technische Wissenschaften
Institut für Informatik-Systeme
|
AT - A-9020 Klagenfurt |
Kategorisierung
Sachgebiete | |
Forschungscluster | Kein Forschungscluster ausgewählt |
Vortragsfokus |
Klassifikationsraster der zugeordneten Organisationseinheiten:
|
TeilnehmerInnenkreis |
|
Publiziert? |
|
Arbeitsgruppen |
|
Kooperationen
Forschungsaktivitäten
(Achtung: Externe Aktivitäten werden im Suchergebnis nicht mitangezeigt)
Projekte |
|
Publikationen | Keine verknüpften Publikationen vorhanden |
Veranstaltungen | Keine verknüpften Veranstaltung vorhanden |
Vorträge | Keine verknüpften Vorträge vorhanden |