This page is for downloading the SAL files for the two case studies used in paper "Compensation by Design" by Xi Liu, Shaofa Yang and J.W. Sanders.

Batch-ATM: ATM.sal
Bank-transfer: Transfer.sal

Some library files are also made, please download and add them to your SAL-PATH in order to run the model checker.
Additional library: lib.zip.

Sample command line:
sal-bmc -v 3 --delta-path ATM DoOp_aonpple --depth=50
sal-bmc -v 3 --delta-path Transfer PayIST_aonpple --depth=80

For how to install and use SAL, please refer to: sal.csl.sri.com