×

SAL

swMATH ID: 13318
Software Authors: Grégoire Hamon, Leonardo de Moura, John Rushby
Description: SAL. The Symbolic Analysis Laboratory 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. The SAL toolkit provides several tools for examining SAL specifications, including three different high-performance model checkers for LTL: symbolic, bounded, and infinite-bounded. The infinite-bounded model checker uses Yices to provide bounded model checking for systems defined over infinite data types, such as integers and reals. In addition, both the bounded and infinite-bounded model checkers can prove invariants by k-induction. SAL has been available since 2002, and has been Open Source since Version 3.0, released in December 2006.
Homepage: http://sal.csl.sri.com/
Related Software: SPIN; PVS; RAISE; HybridSal; AETG; Simulink; StateFlow; Matlab; JPAX; NuSMV; EUREKA; CBMC; Yices
Referenced in: 5 Publications

Standard Articles

1 Publication describing the Software, including 1 Publication in zbMATH Year
SAL 2. Zbl 1103.68644
de Moura, Leonardo; Owre, Sam; Rueß, Harald; Rushby, John; Shankar, N.; Sorea, Maria; Tiwari, Ashish
2004

Referencing Publications by Year