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.
A rigorous empirical study of the impact of miscompilation bugs in a mature compiler, comparing bugs found using a fuzzer to bugs found while compiling real code.
An empirical study and the underlying infrastructure for analyzing code,
test and coverage evolution in real software using both static and
We study the effect of relaxing too conservative conditions for generating UB-free compiler test-cases of Csmith’s code-generation and code-execution time solutions.
Combines dynamic symbolic execution with several novel
heuristics based on program analysis to automatically and comprehensively
test code patches.
A set of semantic-preserving transformations that take advantage of
contextual information collected during symbolic execution to speedup
An extension to KLEE that provides an integer solver based on Z3. Solver queries that do not contain bitvector instructions are forwarded to an integer solver instead of a bitvector solver.
An extension to the KLEE symbolic execution engine that supports
reasoning about floating-point arithmetic and a benchmark set used to evaluate the tool.
A counterexample-guided inductive synthesis approach for summarizing
simple string loops written in C with equivalent sequences of standard library functions and primitive pointer operations.
An approach that combines Dynamic Software Updating (DSU) with Multi-Version Execution (MVE) in order to improve the reliability of software updates and avoid live update delays in services.
A memoization extension for KLEE.
With MoKlee, solver results can be re-used between executions and divergence detection ensures that re-executed paths are valid.
A study of correctness of PDF documents and PDF document readers, based on
clustering errors emitted by the PDF readers and visual inconsistencies detection.
An on-demand pointer analysis integrated with symbolic execution that is
instantiated with an abstraction of the dynamic state on which it is invoked.
A variation on standard symbolic execution, where
expensive branch feasibility checks are delayed until they are necessary for
further exploration of the program.
SaBRe is a modular selective binary rewriter. It is able to rewrite system
calls, vDSO and named functions. We currently support two architectures: x86_64
A segmented memory model for symbolic execution that tackles the issue of symbolic pointer dereferences by leveraging static pointer alias analysis.
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 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 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
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.
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
A symbolic execution engine for the Boogie intermediate verification
language which provides modular components that can be reused in other
A lightweight symbolic execution technique for improving existing test
suites by thoroughly checking for errors all sensitive operations
executed by the test suite.