Reasoning about Heap Manipulating Programs using Automata Techniques
Supratik Chakraborty · Co-Published with Indian Institute of Science (IISc), Bangalore, India eBooks · 2012
Automatically reasoning about programs is of significant interest to the program verification, compiler development and software testing communities. While prop-erty checking for programs is undecidable in general, techniques for reasoning about specific classes of properties have been developed and successfully applied in practice. In this article, we discuss three automata based techniques for reason-ing about programs that dynamically allocate and free memory from the heap. Specifically, we discuss a regular model checking based approach, an approach based on storeless semantics of programs and Hoare-style reasoning, and a counter automaton based approach. Automata theory has been a key area of study in computer science, both for the the-oretical significance of its results as well as for the remarkable success of automata based techniques in diverse application areas. Interesting examples of such appli-cations include pattern matching in text files, converting input strings to tokens