Büchi, Lindenbaum, Tarski: A Program Analysis Appetizer
Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence. Pages 4150-4153.
Abstract
One can prove that a 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 Büchi 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.
@inproceedings{ijcai2016p620,
title = {Büchi, Lindenbaum, Tarski: A Program Analysis Appetizer},
author = {D'Silva, Vijay and Urban, Caterina},
booktitle = {Proceedings of the Twenty-Fifth International Joint Conference on
Artificial Intelligence, {IJCAI-16}},
publisher = {AAAI Press / International Joint Conferences on Artificial Intelligence},
editor = {Subbarao Kambhampati},
pages = {4150--4153},
year = {2016},
month = {7},
url = {https://ijcai.org/proceedings/2016/620},
}
TY - CPAPER TI - Büchi, Lindenbaum, Tarski: A Program Analysis Appetizer AU - D'Silva, Vijay AU - Urban, Caterina T2 - Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI-16 PB - AAAI Press / International Joint Conferences on Artificial Intelligence PY - 2016 SP - 4150 EP - 4153 UR - https://ijcai.org/proceedings/2016/620 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
