Campus Event Calendar
Event Entry
What and Who
Guiding program analyzers toward unsafe executions
Dr. Maria Christakis
University of Kent
SWS Colloquium
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.
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Monday, 6 February 2017
10:00
-- Not specified --
G26
111
Kaiserslautern
Abstract
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.
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.
Contact
Vera Schreiber
--email hidden
Video Broadcast
Yes
Saarbrücken
E1 5
029
passcode not visible
logged in users only
Vera Schreiber, 01/26/2017 13:18 -- Created document.