[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