Skip to main content

Synthesis of Symbolic Input-Output Specifications with Sigma*

Domagoj Babic
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: