Synchronization-Aware Analysis of Asynchronous Programs

Experiments and proofs to selected results for a SPIN 2014 paper submission.

The full version of our submission is here

Requirements

Reproducing our experiments requires the following tools to be installed, and accessible in your path.

  • Ruby, and the eventmachine, colorize, and curses gems -- a gem in installed via the command gem install <gem-name>. Our submission results were reported with Ruby version 2.1.0p0.

  • c2s-ocaml -- our submissions results were reported with commit #5a5a804.

  • Boogie

  • Corral

Note: See the SMACK install script for help on installing Boogie and Corral.

Usage

Reproduce our experiments by running ./param-tests.rb

Notes

Each .bpl file was generated manually, yet systematically, from the original C# source file, as discovered from their respective sources.