Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop


Show entries of:

this year (2019) | last year (2018) | two years ago (2017) | Notes URL

Action:

login to update

Options:








Author, Editor

Author(s):

Madden, Peter

dblp



Editor(s):

Nebel, Bernhard
Dreschler-Fischer, Leonie

dblp
dblp



BibTeX cite key*:

Madden94a-djki

Title, Booktitle

Title*:

Formal Methods for Automated Program Improvement

Booktitle*:

KI-94: Advances in Artificial Intelligence. Proceedings of the 18th German Annual Conference on Artificial Intelligence

Event, URLs

URL of the conference:


URL for downloading the paper:


Event Address*:

Saarbrücken, Germany

Language:

English

Event Date*
(no longer used):

September 18-23, 1994

Organization:


Event Start Date:

16 September 2019

Event End Date:

16 September 2019

Publisher

Name*:

Springer

URL:


Address*:

Berlin, Germany

Type:


Vol, No, Year, pp.

Series:

Lecture Notes in Artificial Intelligence

Volume:

861

Number:


Month:

September

Pages:

367-378

Year*:

1994

VG Wort Pages:


ISBN/ISSN:


Sequence Number:


DOI:




Note, Abstract, ©

Note:

Also available as Research Report MPI-I-94-238, Max-Planck-Institut für Informatik, Saarbrücken

(LaTeX) Abstract:

Systems supporting the manipulation of non-trivial program code are complex and are at best semi-automatic. However, formal methods, and in particular theorem proving, are providing a growing foundation of techniques for automatic program development (synthesis, improvement, transformation and verification). In this paper we report on novel research concerning: (1) the exploitation of synthesis proofs for the purposes of automatic program optimization by the transformation of proofs, and; (2) the automatic synthesis of efficient programs from standard equational definitions. A fundamental theme exhibited by our research is that mechanical program construction, whether by direct synthesis or transformation, is tantamount to program verification plus higher-order reasoning. The exploitation of the proofs-as-programs paradigm lends our approach numerous advantages over more traditional approaches to program improvement. For example, we are able to automate the identification of efficient recursive data-types which usually correspond to *eureka* steps in ``pure'' transformational techniques such as unfold/fold. Furthermore, all transformed, and synthesized, programs are guaranteed correct with respect to their specifications.



Download
Access Level:


Correlation

MPG Unit:

Max-Planck-Institut für Informatik



MPG Subunit:

Programming Logics Group

Audience:

experts only

Appearance:

MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat



BibTeX Entry:

@INPROCEEDINGS{Madden94a-djki,
AUTHOR = {Madden, Peter},
EDITOR = {Nebel, Bernhard and Dreschler-Fischer, Leonie},
TITLE = {Formal Methods for Automated Program Improvement},
BOOKTITLE = {KI-94: Advances in Artificial Intelligence. Proceedings of the 18th German Annual Conference on Artificial Intelligence},
PUBLISHER = {Springer},
YEAR = {1994},
VOLUME = {861},
PAGES = {367--378},
SERIES = {Lecture Notes in Artificial Intelligence},
ADDRESS = {Saarbr{\"u}cken, Germany},
MONTH = {September},
NOTE = {Also available as Research Report MPI-I-94-238, Max-Planck-Institut für Informatik, Saarbrücken},
}


Entry last modified by Christine Kiesel/AG2/MPII/DE, 03/12/2010
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Uwe Brahm
Created
01/14/1995 06:52:14 PM
Revisions
9.
8.
7.
6.
5.
Editor(s)
Christine Kiesel/AG2/MPII/DE
Christine Kiesel/AG2/MPII/DE
Christine Kiesel/AG2/MPII/DE
Christine Kiesel/AG2/MPII/DE
Christine Kiesel/AG2/MPII/DE
Edit Dates
13/12/95 12:23:05
13/12/95 10:30:51
30/11/95 09:57:04
24/02/95 15:30:15
24/02/95 12:03:05