Editor’s Introduction to the Special Volume on Application of Constraints to Formal Verification
Miroslav N. Velev · Journal on Satisfiability Boolean Modeling and Computation · 2008
During the last eight years, tremendous progress was made in the field of Boolean Satisfiability (SAT).Now SAT solvers are 4 to 5 orders of magnitude faster, and can solve formulas that are 4 to 5 orders of magnitude bigger.SAT is the enabling technology for formal verification-the mathematical proof of correctness of computer systems.Statistics from industrial circuit designs indicate that up to 90% of the engineering effort is spent on verification, which increasingly becomes the bottleneck in developing new products.Formal verification, gaining wider acceptance in industry, has the potential to significantly reduce the design time, while also guaranteeing complete correctness and avoiding costly design bugs that can easily drive a company bankrupt.The seven regular papers and two research notes in this special volume present exciting work on applying SAT to formal verification and related domains.In the first paper, entitled Improved SAT-based Reachability Analysis with Observability Don't Cares, Sean Safarpour and Andreas Veneris from the University of Toronto (Canada), and Rolf Drechsler from Bremen University (Germany) present a SAT-based method for reachability analysis.By accounting for observability don't cares-variables whose values do not affect the formula given the values of other variables-it was possible to achieve up to 4× speedup for unbounded model checking problems, and 1 -2 orders of magnitude reduction of trace sizes, thus simplifying the subsequent debugging.The second paper, Abstraction Refinement with Craig Interpolation and Symbolic Pushdown Systems, is by Javier Esparza, Stefan Kiefer, and Stefan Schwoon from the Technical University of Munich (Germany).They studied how Craig interpolants can be computed efficiently in counterexample-guided abstraction refinement for software model checking.They proposed a new type of interpolant and showed how to treat multiple counterexamples in one refinement cycle, achieving exponential speedups.The third paper, Dependence Graph Based Verification and Synthesis of Hardware/ Software Co-Designs with SAT Related Formulation, is by Masahiro Fujita, Kenshu Seto, and Thanyapat Sakunkonchak from the University of Tokyo (Japan).The authors describe verification and synthesis techniques based on the analysis of System Dependence Graphs by translating the problems to SAT and ILP.The experimental results indicate that the state-of-the-art SAT and ILP solvers can scale for reasonably large designs.The fourth paper is entitled Stressing Symbolic