Automatic verification of time behavior of programs

Automatic verification of software could save companies from huge losses due to errors in their programs. Existing techniques to prevent and detect errors are mainly based on imprecise heuristics which can report false positives. Formal verification techniques are an alternative to the heuristic approaches. They are more precise and can report errors with higher rigor. However, they cannot be directly applied because current programming languages have no defined semantics that specifies how the source code is interpreted in the execution of programs. Moreover, no existing work tries to develop a semantics for the time domain. The target of this thesis is to provide a verification framework based on a defined time semantics that can help developers to automatically detect time related errors in the behavior of programs. We define a time semantics that allows us to ascribe a meaning to source code statements that alter and use time. Based on the time semantics, we develop an approach to (i) automatically assert time properties and (ii) reverse engineer timed automata, a formal model of the time behavior that is amenable for verification. We plan to evaluate our approaches with quantitative and qualitative studies. The quantitative studies will measure the performance of our approaches in open source projects and the qualitative studies will collect the developers' feedback about the applicability and usefulness of our proposed techniques.

Publikationstyp: Beitrag in Proceedings (Autorenschaft)
Art der Veröffentlichung Online Publikation
Erschienen in: ICSE '18 Proceedings of the 40th International Conference on Software Engineering: Companion Proceeedings
ICSE '18 Proceedings of the 40th International Conference on Software Engineering: Companion Proceeedings
zur Publikation
 ( ACM New York; )
Erscheinungdatum: 27.05.2018
Titel der Serie: -
Bandnummer: -
Erstveröffentlichung: Ja
Version: -
Seite: S. 468 - 471


  • 978-1-4503-5663-3
AC-Nummer: -
Open Access
  • Online verfügbar (nicht Open Access)


Organisation Adresse
Fakultät für Technische Wissenschaften
Institut für Informatik-Systeme
Universitätsstr. 65-67
A-9020  Klagenfurt
zur Organisation
Universitätsstr. 65-67
AT - A-9020  Klagenfurt


  • 101013 - Mathematische Logik
  • 102022 - Softwareentwicklung
Forschungscluster Kein Forschungscluster ausgewählt
Peer Reviewed
  • Ja
  • Science to Science (Qualitätsindikator: II)
Klassifikationsraster der zugeordneten Organisationseinheiten:
  • Software Engineering Research Group


Keine Kooperationspartner ausgewählt

Beiträge der Publikation

Keine verknüpften Publikationen vorhanden