Next Generation of Memory Management for Symbolic Execution
Martin Nowack (TU Dresden)
Systematic testing of applications is essential to modern software development. But manually writing test cases is a tedious process. With symbolic execution, we have one tool at our hand to help us generating test cases and to find bugs automatically. Still, symbolic execution suffers from the path explosion problem: the number of paths through an application grows exponentially with its size. Merging of states reduces this issue by creating more complex formulas putting more pressure on the solver. We recently investigated, how the process of merging states can be improved by enhancing the memory representation of states. We show that - what seems to be counterintuitive in the first place - a more fine-grain representation of memory objects beside the additional work can have a positive impact on the execution and merging of states.
Martin Nowack received his Diploma in Computer Science from TU Dresden in 2009 and is a research assistant since then at the systems engineering chair at TU Dresden. He is a final year Ph.D. student. His research interests are software validation and testing using symbolic execution; and multi-core programming with a focus on transactional memory. He is a maintainer and active contributor of the open source symbolic execution engine KLEE.
Back to EBSIS Events section.