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.