Symbolic Analysis Laboratory
Encyclopedia : S : SY : SYM : Symbolic Analysis Laboratory
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.
External link
From Wikipedia, the Free Encyclopedia. Original article here. Support Wikipedia by contributing or donating.
All text is available under the terms of the GNU Free Documentation License See Wikipedia Copyrights for details.