Google Research

Buchi, Lindenbaum, Tarski: A Program Analysis Appetizer

Proceedings of the International Joint Conference on Artificial Intelligence, AAAI Press (2016) (to appear)


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.

Learn more about how we do research

We maintain a portfolio of research projects, providing individuals and teams the freedom to emphasize specific types of work