Coming to Terms with Quantified Reasoning
Laura Kovacs, Simon Robillard, Andrei Voronkov

TL;DR
This paper develops two first-order theorem proving methods for reasoning about properties of programs manipulating finite term algebras, enabling automated analysis of algebraic data types with improved performance over existing solvers.
Contribution
It introduces two novel approaches for full first-order reasoning about term algebras, implemented in Vampire, enhancing automated verification of algebraic data types.
Findings
Successfully proved many previously unsolvable problems
Vampire outperforms existing SMT solvers on algebraic data type benchmarks
Methods are effective for complex program analysis involving term algebras
Abstract
The theory of finite term algebras provides a natural framework to describe the semantics of functional languages. The ability to efficiently reason about term algebras is essential to automate program analysis and verification for functional or imperative programs over algebraic data types such as lists and trees. However, as the theory of finite term algebras is not finitely axiomatizable, reasoning about quantified properties over term algebras is challenging. In this paper we address full first-order reasoning about properties of programs manipulating term algebras, and describe two approaches for doing so by using first-order theorem proving. Our first method is a conservative extension of the theory of term algebras using a finite number of statements, while our second method relies on extending the superposition calculus of first-order theorem provers with additional inference…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Software Engineering Research
