Software Synthesis using Automated Reasoning

Date: Thursday, February 24, 2011
Speaker: Ruzica Piskac
Venue: TU Vienna

Software synthesis is a technique for automatically generating codegiven a specification. The goal of software synthesis is to make codingeasier while increasing both the productivity of the programmer and thecorrectness of the produced code. Code produced this way is correct byconstruction. However, due to the high computational cost ofsynthesizing code, this idea was not further explored until recently. We arewitnessing a regaining interest in software synthesis that is driven by theincreasing computational power. Today even desktop machines areable to construct code from complex input specifications.

In this talk I will present our new approach to synthesis that relies onthe use of automated reasoning and decision procedures. We handlecomplex specifications by employing efficient algorithms for reasoningabout the domain of the specification. I will describe how togeneralize decision procedures into predictable and complete synthesisprocedures. Here completeness means that the procedure is guaranteed tofind code that satisfies the given specification. Moreover, thesynthesis procedure also outputs preconditions on input values thatguarantee the existence of the output values. As an example, I willexplain how to transform a decision procedure for lineararithmetic into such a synthesis procedure.

I will also outline a synthesis procedure for specifications given inthe form of type constraints. The procedure takes into accountpolymorphic type constraints as well as code behavior and derives codesnippets that use given library functions. We use a first-orderresolution-based theorem prover to solve these constraints and derivecode snippets. The constraints can have multiple solutions and hence thetheorem prover may produce more than one code snippet. Therefore, we usean additional weight function to rank the derived snippets.

These procedures are implemented as extensions to the Scala compiler andI will include a demo in my talk.

Posted in RiSE Seminar