Please see the preliminary notice about AFM09 -- a workshop for PVS, SAL
and Yices users
FormalWare at SRI
The Formal
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.
- PVS
- 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.
-
Yices
- 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.
- SAL
- 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 HybridSAL (June 2007):
a tool for abstracting hybrid systems (specified in an extension of
SAL) to SAL specifications.
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
SRI FM-Wiki.
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.
Last modified: Tue Apr 14 15:50:09 PDT 2009