MPI-INF Logo
Campus Event Calendar

Event Entry

What and Who

Dynamic Symbolic Execution for Software Analysis

Cristian Cadar
Imperial College London
SWS Distinguished Lecture Series

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.
AG 1, AG 2, AG 3, INET, AG 4, AG 5, SWS, RG1, MMCI  
AG Audience
English

Date, Time and Location

Thursday, 7 February 2019
10:30
60 Minutes
G26
111
Kaiserslautern

Abstract

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.

Contact

Susanne Girard
--email hidden

Video Broadcast

Yes
Saarbrücken
E1 5
029
passcode not visible
logged in users only

Susanne Girard, 01/30/2019 12:43 -- Created document.