A symbolic execution engine for the Boogie intermediate verification language which provides modular components that can be reused in other Boogie projects.

Overview

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.

Download

Symbooglix is available on GitHub.

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/ .

Research Support

This research is generously supported by an EPSRC CASE studentship with ARM.