Constraint Solving Challenges in Dynamic Symbolic Execution

In this talk, I will give an overview of our work on designing dynamic symbolic execution techniques for comprehensively testing real programs.
I will discuss the main challenges of this approach in terms of constraint solving and our experience building two practical symbolic execution tools, EXE and KLEE, capable of automatically generating high-coverage test inputs exposing serious bugs and security vulnerabilities in a diverse set of software systems, including file
systems, device drivers, packet filters, network servers and computer vision code.

Cristian Cadar Imperial College London, London, UK

Cristian Cadar is a Lecturer (Assistant Professor) in the Department of Computing at Imperial College London. His research interests span the
areas of computer systems, software engineering and computer security, with an emphasis on building practical tools for improving the reliability and security of software systems. Cristian received a PhD in Computer Science from Stanford University, a B.S. and an M.Eng. in Computer Science from MIT, and a B.S. in Mathematics also from MIT.