Program analysis with boolean logic solvers
Abstract
Modern computation systems are very complex. As a result they are very challenging to
reason about and validate. Validation techniques based on dynamic analysis—testing— are
time consuming and offer no guarantees of correctness. Researchers have proposed static
verification techniques which require no testing and are complete. Existing static verification
techniques that are based on satisfiability of Boolean formulas in conjunctive normal
form validate designs by forcing bounds on the range of variables of a design. Their primary
drawback is that they are limited to designs of relatively low complexity. They translate
a design expressed in an imperative or a declarative high-level description language
to a Boolean formula. There are three limiting aspects of translating high-level designs
to conjunctive normal form. (1.) A small increase in the bound on variable ranges can
cause a large increase in the size of the translated formula. For example, for an undirected
seven-node tree the translation produced one million variables and five million clauses. (2.)
Boolean satisfiability solvers are restricted to using optimizations that apply at the level of
conjunctive normal form formulas. Finally, (3.) the Boolean formulas often need to be
regenerated with higher bounds to ensure the correctness of the translation.
This dissertation proposes the use of sequential circuits, Boolean formulas with
memory elements and hierarchical structures, and sequential circuit solvers to validate highlevel
designs. (1.) Sequential circuits are much more succinct than the pure combinational
conjunctive normal form formulas and preserve the high-level structure of the design. (2.)
Encoding the problem as a sequential circuit enables the use of a number of powerful automated
analysis techniques that have no counterparts for conjunctive normal form formulas.
This dissertation applies sequential analysis to both declarative and imperative designs. The
results show that it can validate designs with bounds that are orders of magnitude larger than
those achievable by the state of the art techniques based on conjunctive normal form analysis.