FormalWare at SRI
Methods and Dependable Systems Program in the Computer Science Laboratory of SRI International has been at the
forefront of Formal Methods research for three decades. During this
period, we have developed several software tools for automated
verification. This page provides an overview of our current tools and
links for downloading them. All these tools are under active
development, extension, and mutual integration.
- The Prototype Verification System is a comprehensive verification
environment: it provides a specification language in which mathematical
theories and conjectures can be specified, together with an interactive
theorem prover. The PVS specification language is a higher-order logic
with a rich type system that supports concise and perspicuous specifications.
Its theorem prover provides powerful automation, with decision procedures for
several theories including real and integer arithmetic. PVS has been available
since 1993, and has been Open Source since Version 4.0, released in December
- is an SMT solver: it decides the satisfiability of propositional formulas
containing uninterpreted function symbols with equality, linear real and integer
arithmetic, scalar types, recursive datatypes, tuples, records, extensional arrays,
fixed-size bit-vectors, quantifiers, and lambda expressions. It's basic
capability resembles the decision procedures of PVS, but in a form that
incorporates many new theoretical and practical insights and delivers vastly
greater performance and scalability. Yices also does MaxSMT (and, dually,
unsat cores) and is competitive as an ordinary SAT and MaxSAT solver. Yices can
be used as a library in any application that requires "embedded deduction". Yices
is used in SAL 3.0 and in PVS 4.0. Yices has been available since August 2006;
its current version is 1.0. Its prototypes Yices 0.1 and Simplics were available
since July 2005 and its predecessor ICS since 2001. Yices 1.0 won every division in
the 2006 SMT Competition.
- The Symbolic Analysis Laboratory is an environment for the exploration and
analysis of concurrent systems specified as transition relations. Its language
includes many of the attractive features of PVS. The SAL toolkit provides several
tools for examining SAL specifications, including three different high-performance
model checkers for LTL: symbolic, bounded, and infinite-bounded. The infinite-bounded
model checker uses Yices to provide bounded model checking for systems defined over
infinite data types, such as integers and reals. In addition, both the bounded and
infinite-bounded model checkers can prove invariants by k-induction.
SAL has been available since 2002, and has been Open Source since Version 3.0, released
in December 2006.
- We have released (as of June 2007) a tool for abstracting hybrid systems (specified
in an extension of SAL) to SAL specifications.
- We are also getting involved in probabilistic inferencing, and have a Probability
Consistency Engine (PCE) tool for reasoning over Markov Logic Networks.
For an introduction to mechanized formal analysis using these tool,
and an overview of their capabilities, please see this tutorial.
The information below is rather outdated,
but we now have an
We're still learning how best to organize and use this new
capability--please join in and help.
For more information on the relationships between the tools and our
plans for their evolution, please see our Roadmap.
Recent papers on the theory, development, and applications of our tools
are available here, while other papers
can be found by by following links to our
personal home pages.
Development of these tools has been funded by SRI International, the
National Science Foundation, the National Aeronautics and Space
Administration, the Naval Research Laboratory, and the Defense
Advanced Research Projects Agency.