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 2006.
- 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 since version 4.0. Yices has been available
since August 2006..
- 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
For an introduction to mechanized formal analysis using these
tool, and an overview of their capabilities, please see this
The information below is rather outdated.
For more information on the relationships between the tools and our
plans for their evolution, please see our
Earlier 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.