Symbolic Analysis Laboratory
From Free net encyclopedia
To become practical for assurance, automated formal methods must be made more scalable, automatic, and cost-effective. Such an increase in scope, scale, automation and utility can be derived from an emphasis on a systematic separation of concerns during verification. SAL (Symbolic Analysis Laboratory) attempts to address these issues. It is a framework for combining different tools to calculate properties of concurrent systems. The heart of SAL is a language, developed from a collaboration between SRI International, Stanford University, UC Berkeley and Verimag, for specifying concurrent systems in a compositional way. Its verification toolbox includes an explicit-state model checker, a symbolic model checker, a witness-producing model checker, and a bounded model checker.