Symbooglix is Symbolic execution engine for the Boogie intermediate verification language
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 reproducing the study describe in our ICST paper can be found at http://symbooglix.github.io/publications/icst16/artifact/ .
This research has been supported by an EPSRC Industrial CASE PhD studentship supported by ARM.