SAL is open source, under the GNU General Public License (GPL). Informally, this means you can get the sources, and do whatever you want with them, except distribute them with software that is not available under a GPL-compatible license. SAL uses a dual license model; if you are interested in alternative licensing terms contact us at

There are two sets of SAL binaries, depending on whether Yices is included. Selecting a SAL distribution with Yices includes requires acceptance of the Yices "click-through" license. Alternatively, you can get a SAL distribution that does not include Yices. If you wish so, it is always possible to download Yices separately at and it will work with any of the binaries.

SAL Version 3.3 (released March 19 2013 + Minor fix July 17, 2013)

SAL 3.3 includes SALenv 3.0 (symbolic, bounded, and infinite-bounded model checkers, and related tools), and, optionally, Yices.

SAL 3.3 Sources

See the included README file for build instructions.

NOTE: SAL 3.3 does not compile with the latest version of bigloo. It is known to compile with bigloo3.4a (may be available here).

SAL 3.3 Binaries with Yices

This is probably the version you want, as some SAL features will not work without Yices. Yices requires agreement to a "click-through" license.

SAL 3.3 Binaries without Yices

Older Versions