Chopper
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.
Compiler Bugs Impact
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.
CsmithEdge
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.
Gmutator
A fuzzing approach for finding edge inputs by first mutating grammars and then using grammar-based fuzzing on the mutated grammars.
GrayC
We propose a coverage-directed, mutation-based approach for fuzzing C compilers and code analysers, inspired by the success of this type of greybox fuzzing in other application domains.
Just Fuzz It
An approach based on coverage-guided fuzzing for determining the satisfiability of SMT constraints, particularly those that involve floating-point arithmetic.
KATCH
Combines dynamic symbolic execution with several novel heuristics based on program analysis to automatically and comprehensively test code patches.
KDAlloc
A new efficient memory allocator for KLEE that supports cross-run and cross-path determinism as well as spatially and temporally distanced allocations.
KLEE with Integer Extension
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.
KLEE-Float
An extension to the KLEE symbolic execution engine that supports reasoning about floating-point arithmetic and a benchmark set used to evaluate the tool.
Loop Summaries
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.
MVEDSUa
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.
MoKlee
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.
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.
PSPA
An on-demand pointer analysis integrated with symbolic execution that is instantiated with an abstraction of the dynamic state on which it is invoked.
PaZZER
We propose optimisations for directed fuzzing techniques (like AFLGo) such that they are better suited for effective CI/CD fuzzing.
Patch Specifications via Product Programs
A way to automatically create product programs for multiple versions of a program, which lets patch specifications be written and checked that describe the intended change, if any.
Pending Constraints
A variation on standard symbolic execution, where expensive branch feasibility checks are delayed until they are necessary for further exploration of the program.
SA-DSE
A project that aims to confirm true positives from static analysers by following their error traces with KLEE. Surprisingly, the traces did not add many benefits when combined with targeted DSE.
SaBRe
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 and RISC-V.
Segmented Memory Model
A segmented memory model for symbolic execution that tackles the issue of symbolic pointer dereferences by leveraging static pointer alias analysis.
Shadow
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.
SnapFuzz
SnapFuzz is an efficient fuzzing framework for network applications which significantly improves fuzzing throughput and eliminates the need for fragile timing delays and clean-up scripts.
Varan
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.
Older Projects
Covrig
An empirical study and the underlying infrastructure for analyzing code, test and coverage evolution in real software using both static and dynamic metrics.
Docovery
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.
KLEE Array
A set of semantic-preserving transformations that take advantage of contextual information collected during symbolic execution to speedup array operations.
KLEE-CL
An effective symbolic execution based technique for crosschecking C and OpenCL applications involving floating point. It has also been called KLEE-FP.
KLEE-MultiSolver
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.
Mx
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.
SymbexNet
A technique that combines symbolic execution with rule-based specifications to find both low- and high-level bugs in network protocol implementations.
Symbooglix
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.
ZESTI
A lightweight symbolic execution technique for improving existing test suites by thoroughly checking for errors all sensitive operations executed by the test suite.