Guest Speaker

Satisfiability-based Program Reasoning and Synthesis

Saurabh Srivastava
Department of Computer Science
University of Maryland, College Park

Feb 16 2010 3:30PM
480 Dreese Labs
All interested parties are invited to attend.
Refreshments will be served prior to talk.

Abstract:

Today, software is ubiquitous - it is deployed on virtually all electronic devices, small and large, including those that are life-and safety-critical. The need for robust, certifiably correct software requires us to develop the theory and tools for mechanically reasoning about, and also automatically generating, programs.

In this talk, I will present the theory and practice behind a novel approach to program reasoning and program synthesis. Program reasoning is the task of verifying a program against its specification, and of inferring the specification given a program. Program synthesis is the task of automatically generating the program corresponding to a specification.

I will describe novel algorithms that reduce program reasoning and synthesis to SAT/SMT solving problems, which permits leveraging the substantial engineering advances present in today's solvers. Our tools based on this theory can reason about expressive properties of programs, e.g., quantified properties, that were beyond the reach of previous techniques. They can also automatically synthesize programs from specifications, e.g., sorting programs and Strassen's matrix multiplication, which was not possible earlier.

Bio:

Saurabh Srivastava is a Ph.D. Candidate in the Programming Languages group at the University of Maryland, College Park. His dissertation work proposes and evaluates a powerful new paradigm for building program analyses and synthesizers. The work has been published at top conferences and has also been instrumental in building interest in the community towards the automatic program synthesis. He has given various invited seminars on the topic.

Host: Bruce Weide

* Saurabh Srivastava is a CSE faculty candidate