This page reports experiments performed as a first step towards the integration of SAFARI with the BOOGIE program verification system (http://boogie.codeplex.com/).

Here you can find examples of programs with loops, the corresponding SAFARI input program and the BOOGIE files with the invariants generated by SAFARI.