IMDEA Software

Iniciativa IMDEA

Inicio > Eventos > Charlas Invitadas > 2010 > Satisfiability-based Program Reasoning and Synthesis
Esta página aún no ha sido traducida. A continuación se muestra la página en inglés.

Saurabh Srivastava

lunes 22 de marzo de 2010

11:00am IMDEA conference room

Saurabh Srivastava, PhD candidate, University of Maryland, USA

Satisfiability-based Program Reasoning and Synthesis


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.