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

[Joseph Kiniry]

Hi Jean-Christophe et al,

On 12 Jan, 2007, at 13:13, Jean-Christophe Filliatre wrote:

> Hi,
>
> I don't know if  this can be of any help for you,  but we also wrote a
> tool recently to convert the Boogie benchmarks to the native syntax of
> other  provers,  including   SMTlib.   More  precisely,  we  translate
> Simplify's  syntax  to the  input  syntax of  the  Why  tool (our  own
> intermediate language,  see http://why.lri.fr/) and then  the Why tool
> can translate it to various provers.
>
> But  our  translation  is  a  trivial  one,  which  does  not  try  to
> (re)discover  any sort.  All Simplify  terms are  mapped  to integers.
> Thus we simply figure out  the arities of functions and predicates.  I
> attach an example of SMTlib file obtained from the Boogie benchmark.
>
> If you are interested by this  tool, you can download Why 2.01 sources
> (at http://why.lri.fr/).
>
> You'll have to type "make bin/simplify2why.opt" to get the Simplify to
> Why translator.   And you'll get  the Why to SMTlib  translation using
> "why --smtlib".
>
> Hope this helps,
> --  
> Jean-Christophe

The versatility of the Why suite, reemphasized during our semi-recent  
meeting in Nijmegen discussed in our very new blog [1], is one of the  
reasons that integrating it into the Mobius [2] tool suite is on our  
ToDo list.

Thanks for pointing out this new translator!

Joe

[1] http://kindsoftware.blogspot.com/
[2] http://mobius.inria.fr/