Home Intro Wiki Docs FAQ Download Mail FM Tools
SAL

Introduction

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.
Home Intro Wiki Docs FAQ Download Mail FM Tools

Last modified: Thu 09 Apr 2015 11:31 PDT
Maintainer: Bruno Dutertre