Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:Guiding program analyzers toward unsafe executions
Speaker:Dr. Maria Christakis
coming from:University of Kent
Speakers Bio:Maria Christakis is currently a lecturer (assistant professor) in the School
of Computing at the University of Kent, England. She was previously a
post-doctoral researcher at Microsoft Research Redmond, USA. She received
her Ph.D. from the Department of Computer Science of ETH Zurich, Switzerland
in the summer of 2015. Maria was awarded with the ETH medal for an
outstanding doctoral thesis. She completed her Bachelor's and Master's
degrees at the Department of Electrical and Computer Engineering of the
National Technical University of Athens, Greece.
Event Type:SWS Colloquium
Visibility:D1, D2, D3, D4, D5, SWS, RG1, MMCI
We use this to send out email in the morning.
Level:AG Audience
Date, Time and Location
Date:Monday, 6 February 2017
Duration:-- Not specified --
Most static program analysis techniques do not fully verify all possible
executions of a program. They leave executions unverified when they do not
check certain properties, fail to verify properties, or check properties
under certain unsound assumptions, such as the absence of arithmetic
overflow. In the first part of the talk, I will present a technique to
complement partial verification results by automatic test case generation.
In contrast to existing work, our technique supports the common case that
the verification results are based on unsound assumptions. We annotate
programs to reflect which executions have been verified, and under which
assumptions. These annotations are then used to guide dynamic symbolic
execution toward unverified program executions, leading to smaller and more
effective test suites.

In the second part of the talk, I will describe a new program simplification
technique, called program trimming. Program trimming is a program
pre-processing step to remove execution paths while retaining equi-safety
(that is, the generated program has a bug if and only if the original
program has a bug). Since many program analyzers are sensitive to the number
of execution paths, program trimming has the potential to improve their
effectiveness. I will show that program trimming has a considerable positive
impact on the effectiveness of two program analysis techniques, abstract
interpretation and dynamic symbolic execution.
Name(s):Vera Schreiber
Video Broadcast
Video Broadcast:YesTo Location:Saarbr├╝cken
To Building:E1 5To Room:029
Meeting ID:
Tags, Category, Keywords and additional notes
Attachments, File(s):
Vera Schreiber/MPI-SWS, 01/26/2017 12:54 PM
Last modified:
Uwe Brahm/MPII/DE, 02/06/2017 07:01 AM
  • Vera Schreiber, 01/26/2017 01:18 PM -- Created document.