Symbooglix is Symbolic execution engine for the Boogie intermediate verification language

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

Check out Symbooglix on GitHub.

Instructions for reproducing the study describe in our ICST paper can be found at http://symbooglix.github.io/publications/icst16/artifact/ .

Research Support

This research has been supported by an EPSRC Industrial CASE PhD studentship supported by ARM.

Publications

• Symbooglix: A Symbolic Execution Engine for Boogie Programs

  Daniel Liew, Cristian Cadar, Alastair F. Donaldson

  IEEE International Conference on Software Testing, Verification and Validation (ICST'16)