A symbolic execution engine for the Boogie intermediate verification language which provides modular components that can be reused in other Boogie projects.
An intermediate verification language (IVL) aims to simplify the task of building a program analysis tools, by decoupling the handling of the semantics of a real world programming language from the method that is used to prove or disprove the correctness of programs. Boogie is one such IVL that already has several frontends (e.g. SMACK, GPUVerify and Dafny) and several backends (e.g. Boogie verifier, Boogaloo and Corral).
We have implemented a new Symbolic Execution engine for the Boogie IVL and provide a large scale evaluation of Symbooglix against five state of the art Boogie based tools: The Boogie verifier, Boogaloo (an existing Symbolic execution engine), Corral, Duality and GPUVerify.
Instructions for obtaining Symbooglix, the other tools used in our study and the benchmarks can be found at https://symbooglix.github.io/publications/icst16/artifact/ .
This research is generously supported by an EPSRC CASE studentship with ARM.