Experiments and proofs to selected results for a SPIN 2014 paper submission.
The full version of our submission is here
Reproducing our experiments requires the following tools to be installed, and accessible in your path.
-
Ruby, and the
eventmachine
,colorize
, andcurses
gems -- a gem in installed via the commandgem install <gem-name>
. Our submission results were reported with Ruby version 2.1.0p0. -
c2s-ocaml -- our submissions results were reported with commit #5a5a804.
Note: See the SMACK install script for help on installing Boogie and Corral.
Reproduce our experiments by running ./param-tests.rb
Each .bpl
file was generated manually, yet systematically, from the original
C# source file, as discovered from their respective sources.