[SMT-LIB] logic for ESC/Java and Boogie benchmarks

[Joseph Kiniry]

Hi Clark, Michal, et al,

On 13 Jan, 2007, at 21:01, Clark Barrett wrote:

>> 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

They are also available in the ESC/Java2 repository and will be part  
of an independent Simplify release we are planning when we finish  
building and testing a new intel/OS X port.

> We've been looking at doing the same translation ourselves, but I'm  
> always
> happy to let someone else do the work :)

We already have a sorted version of the ESC/Java logic (again, in the  
ESC/Java2 CVS repository) and were planning on writing a "lifter"  
ourselves, but Michal, who will be visiting us later this year, seems  
to have jumped on this independently. :)

> We'll take a closer look at your translation and get back to you  
> about it.
>
> -Clark Barrett
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib

Joe
---
Joseph Kiniry
School of Computer Science and Informatics
University College Dublin
http://secure.ucd.ie/
http://srg.cs.ucd.ie/