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.