[SMT-LIB] logic for ESC/Java and Boogie benchmarks
Clark Barrett
barrett at cs.nyu.edu
Sat Jan 13 16:01:41 EST 2007
> While I still haven't got the original Simplify files that were used
> to generate those (maybe somebody has them around?), I have some other
> ESC/Java benchmarks generated by running it on parts of its own source
> code. I also used Boogie benchmarks available on the Spec# web page.
The benchmarks can be found bundled with the Simplify theorem prover. I put up
a tarball of the benchmarks here:
http://www.cs.nyu.edu/~barrett/tmp/simplify_benchmarks.tar.gz
We've been looking at doing the same translation ourselves, but I'm always
happy to let someone else do the work :)
We'll take a closer look at your translation and get back to you about it.
-Clark Barrett
More information about the SMT-LIB
mailing list