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.
Keywords for this software
References in zbMATH (referenced in 9 articles , 1 standard article )
Showing results 1 to 9 of 9.
- Geisler, S.; Haxthausen, A. E.: Stepwise development and model checking of a distributed interlocking system using RAISE (2021)
- Rushby, John: The versatile synchronous observer (2014) ioport
- Rushby, John: The versatile synchronous observer (2012) ioport
- Calvagna, Andrea; Gargantini, Angelo: A formal logic approach to constrained combinatorial testing (2010)
- Fraser, Gordon; Wotawa, Franz: Using model-checkers to generate and analyze property relevant test-cases. (2008) ioport
- Shimizu, Hiroaki; Hamaguchi, Kiyoharu; Kashiwabara, Toshinobu: Approximate invariant property checking using term-height reduction for a subset of first-order logic (2008)
- Hamon, Grégoire; Rushby, John: An operational semantics for stateflow (2007) ioport
- de Moura, Leonardo; Owre, Sam; Rueß, Harald; Rushby, John; Shankar, N.; Sorea, Maria; Tiwari, Ashish: SAL 2 (2004)
- Moura, Leonardo de; Owre, Sam; Rueß, Harald; Rushby, John; Shankar, Natarajan: The ICS decision procedures for embedded deduction (2004)