FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
A FOOLish Encoding of the Next State Relations of Imperative Programs

Authors: Evgenii Kotelnikov, Laura Kovacs and Andrei Voronkov

Paper Information

Title:A FOOLish Encoding of the Next State Relations of Imperative Programs
Authors:Evgenii Kotelnikov, Laura Kovacs and Andrei Voronkov
Proceedings:IJCAR Proceedings 9th IJCAR, 2018
Editors: Stephan Schulz, Didier Galmiche and Roberto Sebastiani
Keywords:automated theorem proving, next state relation, static analysis, program verification, vampire
Abstract:

ABSTRACT. Automated theorem provers are routinely used in program analysis and verification for checking program properties. These properties are translated from program fragments to formulas expressed in the logic supported by the theorem prover. Such translations can be complex and require deep knowledge of how theorem provers work in order for the prover to succeed on the translated formulas. Our previous work introduced FOOL, a modification of first-order logic that extends it with syntactical constructs resembling features of programming languages. One can express program properties directly in FOOL and leave translations to plain first-order logic to the theorem prover. In this paper we present a FOOL encoding of the next state relations of imperative programs. Based on this encoding we implement a translation of imperative programs annotated with their pre- and post-conditions to partial correctness properties of these programs. We present experimental results which demonstrate that program properties translated using our method can be efficiently checked by the first-order theorem prover Vampire.

Pages:16
Talk:Jul 15 16:30 (Session 107E: Verification)
Paper: