SAL stands for Symbolic Analysis Laboratory. It is a framework for
combining different tools for abstraction, program analysis, theorem
proving, and model checking toward the calculation of properties
(symbolic analysis) of transition systems. A key part of the SAL
framework is an intermediate language for describing transition
systems. This language is intended to serve as the target for
translators that extract the transition system description for other
modeling and programming languages, and as a common source for
driving different analysis tools.
The SAL intermediate language is not that different from the input languages
used by various other verification tools such as
SMV,
Murphi, and
Mocha,
Like these languages, SAL describes transition systems in terms of
initialization and transition commands. These can be given by
variable-wise definitions in the style of SMV
or as guarded commands in
the style of Murphi.
The current generation of SAL tools comprises a collection of state of
the art LTL model checkers and auxiliary tools based on them.
In future
we expect to add tools for static analysis, invariant generation,
abstraction, and a tool bus to connect these together.
The SAL 3.0 distribution (and subsequent releases) includes the
following primary tools. These are fully operational and are
maintained by us.
- sal-wfc
- The SAL well-formedness checker; this is
a limited typechecker for SAL. You should not apply other SAL tools
until any errors identified by the well-formedness checker have been
corrected. Note that sal-wfc is not a full typechecker, so
some type-incorrect SAL specifications will escape detection and
produce unpredictable results. As an intermediate language, SAL is
expected to be mechanically (and correctly) generated from some other
notation, which has its own typechecker.
- sal-smc
- The SAL symbolic model checker; this is
a BDD-based model checker for finite state systems. SAL uses the CUDD BDD package and
provides access to many options for variable ordering, and for
clustering and partitioning the transition relation. The model
checker can perform both forward and backward search, and also
prioritized traversal.
- sal-deadlock-checker
- An auxiliary tool, based on the
symbolic model checker, for detecting deadlocks in finite state
systems.
- sal-bmc
- The SAL bounded model checker; this is a
model checker for finite state systems based on SAT solving. In
addition to refutation (i.e., bug detection and counterexample
generation), the SAL bounded model checker can perform verification by
k-induction. SAL can use several SAT solvers, but defaults to Yices.
- sal-inf-bmc
- The SAL infinite bounded model checker;
this is a model checker for infinite state systems based on SMT
solving. In addition to refutation (i.e., bug detection and
counterexample generation), the SAL infinite bounded model checker can
perform verification by k-induction. SAL can use several SMT solvers,
but defaults to Yices.
- sal-atg
- The SAL automated test generator; this
is an auxiliary tool that uses the symbolic, bounded, and infinite
bounded model checkers to perform automated generation of input
sequences determined by specified trap variables.
The SAL tools are scripts, written in Scheme, that invoke functions of
the SAL API; sal-atg is a good model for those who wish to
develop their own scripts.
- salenv-exec
- The actual SAL executable. All the
other SAL tools are scripts on the API of salenv-exec;
salenv-exec-safe is a version with more error detection,
while salenv and salenv-safe are the top-level shell
scripts invoked by other SAL tools.
In addition, the distribution includes the following experimental
tools. These are incomplete and may be buggy; we do not undertake to
maintain them. They are made available so that others can experiment
with their capabilities or build on their source.
- sal-sim
- The SAL simulator; this is an
interactive front end to other SAL tools.
- sal-wmc
- The SAL witness model checker; this is
an experimental CTL model checker.
- sal-path-finder
- An auxiliary tool, based on the bounded
model checker, that generates random paths.
- sal-emc
- The SAL explicit state model checker.
- sal-path-explorer
- An auxiliary tool, based on the
explicit state model checker.
- ltl2buchi
- An auxiliary tool that generates
(visualizations of) Buchi automata from SAL LTL formulas.
