Symbolic Execution

Lead Research Organisation: Imperial College London
Department Name: Dept of Computing

Abstract

The goal of this research project is to advance techniques for automatic
testing and program analysis. A particular focus will be on symbolic
execution, a technique for automatically exploring program paths. The
research will improve symbolic execution by performing automatic
transformations that make code easier to analyse.

Performance analysis computing

Studentship Projects

Project Reference Relationship Related To Start End Student Name
EP/N509486/1 01/10/2016 30/09/2021
1971026 Studentship EP/N509486/1 01/10/2017 31/03/2021 Timotej Kapus
 
Description We discovered that programmers like to write simple loops instead of using well-known preexisting library functions. These loops presents significant challenge to program analysis tools in general and symbolic execution in particular. We've shown that a an adaptation of existing synthesis techniques can automatically transform these loops into the well-known functions. These transformation can help symbolic execution, but is also applicable to other areas such as compiler optimisation or refactoring tools.
Exploitation Route With moderate engineering effort, our work could be extended to cover more classes of loops and developed into either a refactoring tool, a compiler optimisation or just pre-processing for program analysis.
Sectors Digital/Communication/Information Technologies (including Software)

URL https://srg.doc.ic.ac.uk/projects/loop-summaries/
 
Description Collaboration with Tel Aviv University 
Organisation Tel Aviv University
Country Israel 
Sector Academic/University 
PI Contribution This project led to a close collaboration with Tel Aviv University, which resulted in a joint publication at ICSE 2018.
Collaborator Contribution This project led to a close collaboration with Tel Aviv University, which resulted in a joint publication at ICSE 2018.
Impact Joint paper "Chopped Symbolic Execution" by David Trabish, Andrea Mattavelli, Noam Rinetzky, Cristian Cadar at the International Conference on Software Engineering (ICSE 2018).
Start Year 2017
 
Title KLEE with Integer Extension 
Description 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. 
Type Of Technology Software 
Year Produced 2019 
Open Source License? Yes  
Impact The associated research was published in the International Conference on Tests and Proofs (TAP 2019). The software was used to explore the impact of using the theory of integers on the precision and performance of dynamic symbolic execution of C programs, a topic which was discussed by constraint solving and symbolic execution experts at the 2019 Dagstuhl seminar on "Bringing CP, SAT and SMT together: Next Challenges in Constraint Solving 
URL https://srg.doc.ic.ac.uk/projects/klee-z3-int-vs-bv/
 
Title Loop summarization tool 
Description Analysing and comprehending C programs that use strings is hard: Using standard library functions for manipulating strings is not enforced and programs often use complex loops for the same purpose. We introduce the notion of memoryless loops that capture some of these string loops. The tool uses a counterexample-guided inductive synthesis approach to summarise memoryless string loops using C standard library functions. 
Type Of Technology Software 
Year Produced 2019 
Open Source License? Yes  
Impact The associated research was published in the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2019), one of the top programming languages venues, and the artifact was validated as functional by the PLDI 2019 Artifact Evaluation Committee. The software was used to generate refactoring patches, which were successfully contributed to several popular open-source software systems. 
URL https://srg.doc.ic.ac.uk/projects/loop-summaries/
 
Title Segmented Memory Model for KLEE 
Description Symbolic execution is an effective technique for exploring paths in a program and reasoning about all possible values on those paths. However, the technique still struggles with code that uses complex heap data structures, in which a pointer is allowed to refer to more than one memory object. In such cases, symbolic execution typically forks execution into multiple states, one for each object to which the pointer could refer. This extension avoids this expensive forking by using a segmented memory model. In this model, memory is split into segments, so that each symbolic pointer refers to objects in a single segment. The size of the segments are bound by a threshold, in order to avoid expensive constraints. This results in a memory model where forking due to symbolic pointer dereferences is significantly reduced, often completely. 
Type Of Technology Software 
Year Produced 2019 
Open Source License? Yes  
Impact The associated research was published in the ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE 2019), one of the top software engineering venues, and the artifact was validated as reusable by the ESEC/FSE 2019 Artifact Evaluation Committee. 
URL https://srg.doc.ic.ac.uk/projects/klee-segmem/