Model Checking Software Programs with First Order Logic Specifications using AIG Solvers

TL;DR

This paper introduces a novel approach for software model checking that uses sequential circuits and their synthesis frameworks to verify programs against first order logic specifications, overcoming limitations of traditional SAT/SMT methods.

Contribution

The authors propose a method leveraging sequential circuits for program verification, preserving high-level structure and enabling advanced analysis techniques not available with standard Boolean formulae.

Findings

Sequential circuits are more succinct than Boolean formulae without memory.

Encoding programs as sequential circuits allows use of powerful automated analysis techniques.

The method effectively verifies programs against first order logic specifications within variable bounds.

Abstract

Static verification techniques leverage Boolean formula satisfiability solvers such as SAT and SMT solvers that operate on conjunctive normal form and first order logic formulae, respectively, to validate programs. They force bounds on variable ranges and execution time and translate the program and its specifications into a Boolean formula. They are limited to programs of relatively low complexity for the following reasons. (1) A small increase in the bounds can cause a large increase in the size of the translated formula. (2) Boolean satisfiability solvers are restricted to using optimizations that apply at the level of the formula. Finally, (3) the Boolean formulae often need to be regenerated with higher bounds to ensure the correctness of the translation. We present a method that uses sequential circuits, Boolean formulae with memory elements and hierarchical structure, and sequential circuit synthesis and verification frameworks to validate programs. (1) Sequential circuits are much more succinct than Boolean formulae with no memory elements and preserve the high-level structure of the program. (2) Encoding the problem as a sequential circuit enables the use of a number of powerful automated analysis techniques that have no counterparts for other Boolean formulae. Our method takes an imperative program with a first order logic specification consisting of a precondition and a postcondition pair, and a bound on the program variable ranges, and produces a sequential circuit with a designated output that is true when the program violates the specification.