Automated program verification

Azadeh Farzan, Matthias Heizmann, Jochen Hoenicke, Zachary Kincaid, Andreas Podelski

Research output: Chapter in Book/Report/Conference proceedingConference contribution

4 Scopus citations

Abstract

A new approach to program verification is based on automata. The notion of automaton depends on the verification problem at hand (nested word automata for recursion, Büchi automata for termination, a form of data automata for parametrized programs, etc.). The approach is to first construct an automaton for the candidate proof and then check its validity via automata inclusion. The originality of the approach lies in the construction of an automaton from a correctness proof of a given sequence of statements. A sequence of statements is at the same time a word over a finite alphabet and it is (a very simple case of) a program. Just as we ask whether a word has an accepting run, we can ask whether a sequence of statements has a correctness proof (of a certain form). The automaton accepts exactly the sequences that do.

Original languageEnglish (US)
Title of host publicationLanguage and Automata Theory and Applications - 9th International Conference, LATA 2015, Proceedings
PublisherSpringer Verlag
Pages25-46
Number of pages22
ISBN (Electronic)9783319155784
DOIs
StatePublished - Jan 1 2015
Externally publishedYes
Event9th International Conference on Language and Automata Theory and Applications, LATA 2015 - Nice, France
Duration: Mar 2 2015Mar 6 2015

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8977
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other9th International Conference on Language and Automata Theory and Applications, LATA 2015
CountryFrance
CityNice
Period3/2/153/6/15

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Automated program verification'. Together they form a unique fingerprint.

  • Cite this

    Farzan, A., Heizmann, M., Hoenicke, J., Kincaid, Z., & Podelski, A. (2015). Automated program verification. In Language and Automata Theory and Applications - 9th International Conference, LATA 2015, Proceedings (pp. 25-46). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8977). Springer Verlag. https://doi.org/10.1007/978-3-319-15579-1_2