Examples of translations to Boogie

Apr 14, 2014 at 10:12 PM
Hello, are there are some examples of translations of source code to their Boogie representations (other than the simple example in the user guide)? I see lots of examples in the Test directory but alas only the Boogie code, not the source file from whence they came.

thanks
Apr 15, 2014 at 3:45 PM
Verifiers that use Boogie as the back-end usually have a command-line option to output the generated Boogie code, so you can produce as many translation examples as you like. E.g., for the Dafny verifier use "dafny -print:out.bpl in.dfy" to get the Boogie translation of "in.dfy" in "out.bpl".
For the AutoProof verifier you can get a Boogie translation through the web interface: go to http://cloudstudio.ethz.ch/comcom/#AutoProof, "More AutoProof", and enter "-nadia" in the command line. Then copy-paste any of the examples into the text editor and click "run".

Hope this helps!
Nadia
Apr 29, 2014 at 12:21 PM
Hi snedunuri

Our GPUVerify tool translated OpenCL kernels into Boogie. You might find it useful to run the tool on the test suite and look at the temp files that are generated. Let me know if you do this and if you need help.

http://multicore.doc.ic.ac.uk/tools/GPUVerify/

Ally


On 14/04/2014 22:12, snedunuri wrote:

From: snedunuri

Hello, are there are some examples of translations of source code to their Boogie representations (other than the simple example in the user guide)? I see lots of examples in the Test directory but alas only the Boogie code, not the source file from whence they came.

thanks