Buchi, Lindenbaum, Tarski: A Program Analysis Appetizer

One can prove that a program program satisfies a correctness property in different ways. The deductive approach uses logic and is automated using decision procedures and proof assistants. The automata-theoretic approach reduces questions about programs to algorithmic questions about automata. In the abstract interpretation approach, programs and their properties are expressed in terms of fixed points in lattices and reasoning uses fixed point approximation techniques. We describe a research programme to establish precise, mathematical correspondences between these approaches and to develop new analyzers using these results. The theoretical tools we use are the theorems of Buchi that relate automata and logic and a construction of Lindenbaum and Tarski for generating lattices from logics. This research has lead to improvements in existing tools and we anticipate further theoretical and practical consequences.

• Algorithms and Theory