Symbolic finite-state model checking is a technique for analyzing properties of computational systems. This project rethinks symbolic model checking to achieve scalable performance on multi-core and networked computers. Current attempts to parallelize model checking use standard algorithms and techniques, but this project takes a new approach in which parallel threads share Boolean clauses, which are lemmas of the final proof. It is hypothesized that such clauses represent the appropriate quantum of shared information for parallelization: neither so simple as to cause excessive communication, nor so complex as to cause threads to duplicate work. If the hypothesis is correct, implementations will achieve near-linear scaling with the number of computer cores. The work also investigates the tradeoffs between verifying correctness of properties versus checking properties for counterexamples, exploring performance implications of the tradeoffs.
Symbolic model checking has applications in a wide range of areas, from verifying sequential circuits and security protocols to analyzing biological processes. Advances in model checking allow one to analyze systems of increasingly higher complexity. The project will integrate research and education by developing curriculum that increases the workforce's proficiency in logic, as well as develop educational material on computational thinking for secondary school students.
This project resulted most significantly in the invention of the IC3 algorithm for model checking properties of computer designs. Scalable model checking contributes to the overall robustness of computer hardware designs, yielding safe hardware on which to build cyber-physical systems such as medical equipment, automobiles, and communication networks. Chip designers also gain efficiency through decreased testing costs. In the computer hardware industry, hardware model checking complements testing by offering the assurance of proof. However, model checking is a notoriously hard problem. The method pioneered in the IC3 model checker exploits two complementary sources of scalability to enable the use of formal methods on larger designs: property-focused abstraction and parallel execution. IC3 generates many local intermediate lemmas on its way to a proof, and in so doing focuses its attention on aspects of the design relevant to proving the property. Additionally, IC3 distributes the task of discovering the intermediate lemmas among communicating processors, exhibiting performance that scales linearly with the number of processors. The algorithm has had a significant impact. IC3 demonstrates a breakthrough in hardware model checking. In the 2010 Hardware Model Checking Competition (HWMCC'10), IC3 placed third, "marginally outperformed by two mature integrated verification systems.... [It] appears to be the most important contribution to bit-level formal verification in almost a decade," according to a leading research group at UC Berkeley. After IC3's performance at HWMCC'10, R&D teams at IBM, Cadence, and Microsoft Research, among others, as well as academic teams around the world have implemented the algorithm. They report that the method succeeds on properties and designs that existing techniques are unable to solve. Follow-up work by the inventor and collaborators, which extends the approach to other types of temporal properties, won the best paper award at FMCAD 2011. And IC3 itself just won the HVC Award for 2012, which "recognizes the most promising academic and industrial contribution to the fields of testing and software and hardware verification from the last five years."
