Welcome
Welcome to formalware.csl.sri.com, the
one-stop site for the state-of-the-art tools for mechanized formal
methods developed by the Formal Methods and
Dependable Systems Program in the Computer
Science Laboratory of SRI
International.
Our tools are freely available for noncommercial research purposes
under the terms of our FM License. For commercial
applications, please contact ZZZZZ.
Our Tools
We provide three different tools; each provides unique capabilities
and is intended for particular classes of applications, but all three
share a common vision and there are synergies between them.
The links below lead to the home pages for each of our tools.
PVS is a classical ``verification system'': it provides a
specification language in which mathematical theories and conjectures
about them can be specified, together with an interactive theorem
prover that is used to discharge the conjectures. 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.
Conceptually, ICS is the decision procedures of PVS made available as
a standalone C library that can be embedded in any application that
requires "embedded deduction". However, ICS incorporates many new
theoretical and practical insights and its performance and scalability
vastly exceed those of the PVS decision procedures. Furthermore, ICS
includes a propositional satisfiability (SAT) solver and is able to
solve propositionally complex formulas over the decided theories.
SAL 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 and has both textual and XML
representations: the latter makes it convenient to use SAL as a
backend to other systems. The SAL toolkit provides four different
model checkers: an explicit-state model checker in SALenv-1, and
symbolic, bounded, and infinite-bounded model checkers in SALenv-2.
The infinite-bounded model checker uses ICS to provided bounded model
checking for systems defined over infinite data types, such as
integer and real numbers.
Roadmap
In the near future, we expect to release a version of PVS that can use
ICS as its decision procedure, and a SAL Tool Bus that will
provide an open environment for interoperation of many tools.
For more information on the relationships between the tools and our
plans for their evolution, please see our roadmap.
Papers
Papers on the theory, development, and applications of our tools can be
found by following links to our personal home pages from the home page
for the
Formal Methods and
Dependable Systems program.