Chopped symbolic execution is a novel form of symbolic execution which allows users to specify uninteresting parts of the code which can be excluded during analysis.


An empirical study and the underlying infrastructure for analyzing code, test and coverage evolution in real software using both static and dynamic metrics.


Combines dynamic symbolic execution with several novel heuristics based on program analysis to automatically and comprehensively test code patches.

KLEE Array

A set of semantic-preserving transformations that take advantage of contextual information collected during symbolic execution to speedup array operations.


An extension to the KLEE symbolic execution engine that supports reasoning about floating-point arithmetic and a benchmark set used to evaluate the tool.


An extension to KLEE that uses the metaSMT framework to add support for multiple SMT solvers (Boolector, STP and Z3), and its evaluation on 12 Coreutils applications.

PDF Errors

A study of correctness of PDF documents and PDF document readers, based on clustering errors emitted by the PDF readers and visual inconsistencies detection.


A symbolic execution-based technique for patch testing. The old and the new version are run simultaneously in order to discover the introduced behavioural divergences.


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

Testing SymEx Engines

A technique for testing symbolic execution engines based on program generation and differential testing of compilers, together with a case study on CREST, KLEE and FuzzBall.


An NVX framework that combines selective binary rewriting with a novel event-streaming architecture to significantly reduce performance overhead and scale well with the number of versions.


A lightweight symbolic execution technique for improving existing test suites by thoroughly checking for errors all sensitive operations executed by the test suite.

Older Projects


A novel document recovery technique based on symbolic execution that makes it possible to fix broken documents without any prior knowledge of the file format.


An effective symbolic execution based technique for crosschecking C and OpenCL applications involving floating point. It has also been called KLEE-FP.


A novel multi-version execution technique for surviving buggy software updates, whose key insight is to run the new software version in parallel with the old one.


A technique that combines symbolic execution with rule-based specifications to find both low- and high-level bugs in network protocol implementations.