Satisfiability-based Program Reasoning and Program Synthesis

Simple item page
dc.contributor.advisorFoster, Jeffrey Sen_US
dc.contributor.authorSrivastava, Saurabhen_US
dc.contributor.departmentComputer Scienceen_US
dc.contributor.publisherDigital Repository at the University of Marylanden_US
dc.contributor.publisherUniversity of Maryland (College Park, Md.)en_US
dc.date.accessioned2010-07-02T06:09:58Z
dc.date.available2010-07-02T06:09:58Z
dc.date.issued2010en_US
dc.description.abstractProgram reasoning consists of the tasks of automatically and statically verifying correctness and inferring properties of programs. Program synthesis is the task of automatically generating programs. Both program reasoning and synthesis are theoretically undecidable, but the results in this dissertation show that they are practically tractable. We show that there is enough structure in programs written by human developers to make program reasoning feasible, and additionally we can leverage program reasoning technology for automatic program synthesis. This dissertation describes expressive and efficient techniques for program reasoning and program synthesis. Our techniques work by encoding the underlying inference tasks as solutions to satisfiability instances. A core ingredient in the reduction of these problems to finite satisfiability instances is the assumption of templates. Templates are user-provided hints about the structural form of the desired artifact, e.g., invariant, pre- and postcondition templates for reasoning; or program templates for synthesis. We propose novel algorithms, parameterized by suitable templates, that reduce the inference of these artifacts to satisfiability. We show that fixed-point computation---the key technical challenge in program reasoning---is encodable as SAT instances. We also show that program synthesis can be viewed as generalized verification, facilitating the use of program reasoning tools as synthesizers. Lastly, we show that program reasoning tools augmented with symbolic testing can be used to build powerful synthesizers with approximate guarantees. We implemented the techniques developed in this dissertation in the form of the VS3---Verification and Synthesis using SMT Solvers---suite of tools. Using the VS3 tools, we were able to verify and infer expressive properties of programs, and synthesize difficult benchmarks from specifications. These prototype tools demonstrate that we can exploit the engineering advances in current SAT/SMT solvers to do automatic program reasoning and synthesis. We propose building future automatic program reasoning and synthesis tools based on the ideas presented in this dissertation.en_US
dc.identifier.urihttp://hdl.handle.net/1903/10416
dc.subject.pqcontrolledComputer Scienceen_US
dc.subject.pqcontrolledApplied Mathematicsen_US
dc.subject.pqcontrolledComputer Engineeringen_US
dc.subject.pquncontrolledFixed-point Computationen_US
dc.subject.pquncontrolledProgram Reasoningen_US
dc.subject.pquncontrolledVerification and Specification Inferenceen_US
dc.subject.pquncontrolledProgram Synthesisen_US
dc.subject.pquncontrolledSAT/SMT Solversen_US
dc.subject.pquncontrolledTemplatesen_US
dc.subject.pquncontrolledVS3en_US
dc.titleSatisfiability-based Program Reasoning and Program Synthesisen_US
dc.typeDissertationen_US

Files

Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
Srivastava_umd_0117E_11263.pdf
Size:
1.32 MB
Format:
Adobe Portable Document Format
Download

Collections

UMD Theses and Dissertations
Computer Science Theses and Dissertations