New Class of Formal Verification Engines Reaching Maturity
MENLO PARK, Calif. -- September 26, 2006 -- SRI International's "Yices" technology won a competition of formal verification engines at the Conference on Automated Verification (CAV) held in Seattle, Washington on August 20, 2006. The competition highlighted the arrival of a new class of engines that can address satisfiability modulo theories (SMT). The best of these verifiers now have wide capabilities and very impressive performance.
Formal verification is used to prove the properties of a system or to prove that it does not have a certain defect. Formal verification goes beyond software testing and is particularly important in systems such as those used for drive-by-wire, fly-by-wire and other safety critical systems.
SRI's Yices engine achieved the best performance at this year's competition, receiving first place ranking in every division of the competition and jointly in two divisions. The competition was divided into 11 divisions according to the combination of theories considered, ranging from difference logic (constraints of the form x - y <= c) through full linear arithmetic for integers and reals, and combinations of these with uninterpreted functions, fixed-size bit vectors, arrays, and quantified formulas. A total of 12 SMT solvers competed, although not all tackled every division. The results showed significant progress over the previous year's competition. In some divisions, the prior year's winner would have trailed all of this year's entrants.
"We're delighted with the performance of our technology at the competition," said Patrick Lincoln, Ph.D., director of SRI's Computer Science Laboratory where Yices was developed. "The design team should be congratulated for their outstanding achievement, which reinforces SRI’s position as a leader in this field."
Along with several other related SRI technologies, Yices is currently available for evaluation and licensing at yices.csl.sri.com.
How SMT Solvers Work
SMT solvers work by combining decision procedures for mathematical theories such as linear integer arithmetic with a SAT solver, which assigns a true or false value to all formulas, and these combinations are much more complex and difficult to engineer than a plain SAT solver. Researchers at several universities and institutes around the world have been working on this engineering problem for several years and evaluating different approaches against a collection of benchmark problems. Starting in 2005, a competition for SMT solvers has been held in association with the prestigious Conference on Automated Verification.
Formal Verification Makes Steady Progress
Formal verification is making steady progress in design flows for hardware and is gaining popularity in embedded software and in extended static analysis of mainstream software.
"Deep inside formal verification tools and static analyzers are the core engines that perform symbolic reasoning. These core engines provide the key strength of formal methods, which is the ability to examine all possible executions," said John Rushby, Ph.D., director of SRI’s formal methods program at SRI.
Industrially viable formal verification tools have generally been restricted to finite state systems. Both symbolic model checking (SMC) and bounded model checking (BMC), where binary decision diagrams (BDDs) and propositional satisfiability (SAT) solvers respectively provide the core engines, are restricted to designs represented at the Boolean level. A new wave of tools based on SMT solvers is now available. These tools can perform BMC for infinite state systems and are often faster than SAT-based BMC for finite state systems.
Furthermore, SMT solvers work on higher-level non-Boolean representations using integers and functions so that formal verification can be used much earlier in the design flow and on larger designs. SMT solvers can also decide the "verification conditions" generated by extended static checkers that examine C and Java programs for certain classes of bugs, can contribute to analysis of designs that use real numbers (e.g., those in Matlab/Simulink), and can perform automated generation of test cases.
In related developments, SRI announced that the latest versions of its PVS verification system, which uses interactive theorem proving, and its SAL model checking suite have been extended to use Yices and have switched their licensing terms to open source under the Gnu General Public License (GPL). Custom licensing terms are also available. Visit fm.csl.sri.com for details.
###
About SRI International
Silicon Valley-based SRI International (www.sri.com) is one of the world’s leading independent research and technology development organizations. Founded as Stanford Research Institute in 1946, SRI has been meeting the strategic needs of clients for 60 years. The nonprofit research institute performs client-sponsored research and development for government agencies, commercial businesses, and private foundations. In addition to conducting contract R&D, SRI licenses its technologies, forms strategic partnerships, and creates spin-off companies.
