TY - GEN

T1 - Automated program verification

AU - Farzan, Azadeh

AU - Heizmann, Matthias

AU - Hoenicke, Jochen

AU - Kincaid, Zachary

AU - Podelski, Andreas

PY - 2015/1/1

Y1 - 2015/1/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84928817641&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84928817641&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-15579-1_2

DO - 10.1007/978-3-319-15579-1_2

M3 - Conference contribution

AN - SCOPUS:84928817641

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 25

EP - 46

BT - Language and Automata Theory and Applications - 9th International Conference, LATA 2015, Proceedings

PB - Springer Verlag

T2 - 9th International Conference on Language and Automata Theory and Applications, LATA 2015

Y2 - 2 March 2015 through 6 March 2015

ER -