  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.
