Modular Verification for Almost-Sure Termination of Probabilistic Programs

Guide to the implementation accompanying the paper

Files

Dependencies

Our implementation is written in Java and depends on JavaILP and lpsolve. In order to compile the source codes, you will need both JavaILP and lpsolve. However, JavaILP is embedded in the executable jar file, so in order to run the jar file, you just need to install lpsolve first and make sure that it is in the Java CLASSPATH. This is already taken care of in the virtual machine.

Running the implementation

To run the implementation over an input program “input.prog”, simply execute the following command in a terminal:

java -jar main.jar input.prog

It will try to synthesize a linear DSM-map for the outer-most loop of the input program and writes a log of every step of the process.

Note 1: A DSM-map with epsilon=0 corresponds to failure.

Note 2: The command above will only produce a DSM with respect to the outermost loop. If a program consists of several loops, they should be handled separately (see the programs in examples.zip)

Format of the input

The input program should be written according to the syntax grammar provided in the paper. The invariants should be enclosed between two ‘#’ characters and the program should end with the keyword “end”.  See the examples.

Reproducing the results

There is a script named “run.sh” on the Desktop of the virtual machine. To obtain all the results reported in the paper, simply double-click it and choose “Run in Terminal”. It will run our algorithm on all benchmarks (which are in the “examples” directory). A new directory named “results” will be created which contains a complete log of every run.

Runtime

We expect run.sh to take around 1 minute to execute.

Reading the logs

Each log writes a detailed account of every step of our algorithm (following the paper). The most interesting part of a log is its last part, where it outputs the complete DSM as well as the runtime of our analysis. You can verify the results reported in Tables 1 and 2 and Appendix F.2 by simply looking at this part. Note that in the tables we are only reporting eta(1).

Potential Differences with the paper

Contact address

If you have any difficulty in installing the prerequisites or running the implementation, please contact goharshady@ist.ac.at.