Cristian Cadar

"Dynamic Symbolic Execution for Software Analysis"

( MPI-SWS talk in Kooperation mit dem Fachbereich Informatik)

Symbolic execution is a program analysis technique that can automatically explore and analyse paths through a program. While symbolic execution was initially introduced in the seventies, it has only received significant attention during the last decade, due to tremendous advances in constraint solving technology and effective blending of symbolic and concrete execution into what is often called dynamic symbolic execution. Dynamic symbolic execution is now a key ingredient in many computer science areas, such as software engineering, computer security, and software systems, to name just a few. In this talk, I will discuss recent advances and ongoing challenges in the area of dynamic symbolic execution, drawing upon our experience developing several symbolic execution tools for many different scenarios, such as high-coverage test input generation, bug and security vulnerability detection, patch testing and bounded verification, among many others.

Bio: Cristian Cadar is a Reader in the Department of Computing at Imperial College London, where he leads the Software Reliability Group (http://srg.doc.ic.ac.uk), working on automatic techniques for increasing the reliability and security of software systems. Cristian received an ERC Consolidator Grant in 2018, the HVC Award in 2017, the ACM CCS Test of Time Award in 2016, a British Computer Society Fellowship in 2016, the Jochen Liedtke Young Researcher Award in 2015 and an EPSRC Early-Career Fellowship in 2013. Many of the research techniques he co-authored have been open-sourced and used by several groups in both academia and industry. In particular, he is co-author and the principal maintainer of the KLEE symbolic execution system, a popular system with a large user base. Cristian has a PhD in Computer Science from Stanford University, and undergraduate and Master's degrees from the Massachusetts Institute of Technology.