CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Coming to Terms with Quantified Reasoning

Laura Kovacs (Institutionen för Data- och informationsteknik, Formella metoder (Chalmers)) ; Simon Robillard (Institutionen för Data- och informationsteknik, Formella metoder (Chalmers)) ; Andrei Voronkov (Institutionen för Data- och informationsteknik, Formella metoder (Chalmers))
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages p. 260-270. (2017)
[Konferensbidrag, refereegranskat]

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 rules.
We implemented our work in the first-order theorem prover Vampire and evaluated it on a large number of algebraic data type benchmarks, as well as game theory constraints. Our experimental results show that our methods are able to find proofs for many hard problems previously unsolved by state-of-the-art methods. We also show that Vampire implementing our methods outperforms existing SMT solvers able to deal with algebraic data types.

Nyckelord: program analysis and verification, algebraic data types, automated reasoning, first-order theorem proving, superposition proving



Denna post skapades 2017-01-30. Senast ändrad 2017-04-05.
CPL Pubid: 247905

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)