Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
Zur Ablage hinzufügen
 Lokale TagsFreigabegeschichteDetailsÜbersicht
  Generic System Support for Deductive Program Development

Ayari, A., & Basin, D. A. (1996). Generic System Support for Deductive Program Development. In T. Margaria, & B. Steffen (Eds.), Second International Workshop, TACAS'96: Tools and Algorithms for the Construction and Analysis of Systems (pp. 313-328). Berlin, Germany: Springer.

Item is

 

einblenden: alle ausblenden: alle

Basisdaten

einblenden: ausblenden:
Datensatz-Permalink: https://hdl.handle.net/11858/00-001M-0000-0014-ABDC-E Versions-Permalink: https://hdl.handle.net/11858/00-001M-0000-0014-ABDD-C
Genre: Konferenzbeitrag

Externe Referenzen

einblenden:

Urheber

einblenden:
ausblenden:
 Urheber:
Ayari, Abdelwaheb1, Autor           
Basin, David A.1, Autor           
Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              

Inhalt

einblenden:
ausblenden:
Schlagwörter: -
 Zusammenfassung: We report on a case study in using logical frameworks to support the formalization of programming calculi and their application to deduction-based program synthesis. Within a conservative extension of higher-order logic implemented in the Isabelle system, we derived rules for program development that can simulate those of the deductive tableau proposed by Manna and Waldinger. We have used the resulting theory to synthesize a library of verified programs, focusing on sorting algorithms. Our experience suggests that the methodology we propose is well suited both to implement and use programming calculi, extend them, partially automate them, and even formally reason about their correctness.

Details

einblenden:
ausblenden:
Sprache(n): eng - English
 Datum: 2010-03-121996
 Publikationsstatus: Erschienen
 Seiten: -
 Ort, Verlag, Ausgabe: Berlin, Germany : Springer
 Inhaltsverzeichnis: -
 Art der Begutachtung: -
 Identifikatoren: eDoc: 519622
Anderer: Local-ID: C1256104005ECAFC-DF7E389DE7399656C125630D005F1F68-AbduBasin-TACAS96
 Art des Abschluß: -

Veranstaltung

einblenden:
ausblenden:
Titel: Untitled Event
Veranstaltungsort: Passau, Germany
Start-/Enddatum: 1996

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle 1

einblenden:
ausblenden:
Titel: Second International Workshop, TACAS'96: Tools and Algorithms for the Construction and Analysis of Systems
Genre der Quelle: Konferenzband
 Urheber:
Margaria, Tiziana, Herausgeber
Steffen, Bernhard1, Herausgeber           
Affiliations:
1 Programming Logics, MPI for Informatics, Max Planck Society, ou_40045            
Ort, Verlag, Ausgabe: Berlin, Germany : Springer
Seiten: - Band / Heft: - Artikelnummer: - Start- / Endseite: 313 - 328 Identifikator: ISBN: 3-540-61042-1

Quelle 2

einblenden:
ausblenden:
Titel: Lecture Notes in Computer Science
Genre der Quelle: Reihe
 Urheber:
Affiliations:
Ort, Verlag, Ausgabe: -
Seiten: - Band / Heft: - Artikelnummer: - Start- / Endseite: - Identifikator: -