Combining proof plans with partial order planning for imperative program synthesis

Andrew Ireland, Jamie Stark

Research output: Contribution to journalArticle

4 Citations (Scopus)

Abstract

The structured programming literature provides methods and a wealth of heuristic knowledge for guiding the construction of provably correct imperative programs. We investigate these methods and heuristics as a basis for mechanizing program synthesis. Our approach combines proof planning with conventional partial order planning. Proof planning is an automated theorem proving technique which uses high-level proof plans to guide the search for proofs. Proof plans are structured in terms of proof methods, which encapsulate heuristics for guiding proof search. We demonstrate that proof planning provides a local perspective on the synthesis task. In particular, we show that proof methods can be extended to represent heuristics for guiding program construction. Partial order planning complements proof planning by providing a global perspective on the synthesis task. This means that it allows us to reason about the order in which program fragments are composed. Our hybrid approach has been implemented in a semi-automatic system called Bertha. Bertha supports partial correctness and has been tested on a wide range of non-trivial programming examples.

Original languageEnglish
Pages (from-to)65-105
Number of pages41
JournalAutomated Software Engineering
Volume13
Issue number1
DOIs
Publication statusPublished - Jan 2006

Keywords

  • Deductive synthesis
  • Partial order planning
  • Program synthesis
  • Proof planning

Fingerprint Dive into the research topics of 'Combining proof plans with partial order planning for imperative program synthesis'. Together they form a unique fingerprint.

  • Cite this