Synthesis of Symbolic Input-Output Specifications with Sigma*
- 11:30 11th March 2013 ( week 9, Hilary Term 2013 )278
I will present Sigma*, a novel technique for synthesis of symbolic
models of software behavior. Sigma* addresses the challenge of
synthesizing models of software by using symbolic conjectures and
abstraction. By combining dynamic symbolic execution to discover
symbolic input-output steps of the programs and counterexample guided
abstraction refinement to over-approximate program behavior, Sigma*
transforms arbitrary source representation of programs into faithful
input-output models. I define a class of stream filters --— programs
that process streams of data items --— for which Sigma* converges to a
complete model if abstraction refinement eventually builds up a
sufficiently strong abstraction. In other words, Sigma* is complete
relative to abstraction. Thus, Sigma* enables fully automatic analysis
of behavioral properties such as commutativity, reversibility and
idempotence, which is useful for web sanitizer verification and stream
programs compiler optimizations, as I show experimentally. I also show
how models inferred by Sigma* can boost performance of stream programs
by parallelized code generation.
Speaker bio
Domagoj Babic is a computer scientist at Facebook, Inc. His research focuses on verification, testing, synthesis, and security of complex software (and hardware) systems, automated reasoning and inference of system models, and applied formal methods in general. Before joining Facebook, Domagoj was a research scientist at UC Berkeley and before that in the EDA industry.He received his Dipl.Ing. in Electrical Engineering and M.Sc. in Computer Science from the Zagreb University (Faculty of Electrical Engineering and Computing) in 2001 and 2003. He received his Ph.D. in Computer Science in 2008 from the University of British Columbia.
He is a recipient of the Canada's NSERC PDF Research Fellowship (2010-2012), Microsoft Graduate Research Fellowship (2005-2007), and several awards at international programming competitions (1st place at the 2007 Satisfiability Modulo Theories competition in the bit-vector arithmetic category and 3rd place at the 2005 Satisfiability Testing competition in the satisfiable-crafted instances category).
Share this:
