TUD Technische Universität Darmstadt
Universitäts- und Landesbibliothek
ULB Darmstadt

EPDA - Elektronische Publikationen Darmstadt


Autor: Schweitzer, Dirk Stephan
Titel:Symbolische Auswertung und Heuristiken zur Verifikation funktionaler Programme
Dissertation:TU Darmstadt, Fachbereich Informatik, 2007

Die Dokumente in PDF 1.3 (mit Adobe Acrobat Reader 4.0 zu lesen):

diss-druck.pdf (2067890 Byte)

Abstract auf Deutsch:


Die vorliegende Arbeit beschreibt den im Rahmen des VeriFun-Systems entwickelten symbolischen Auswertungskalkül. Hierbei handelt es sich um einen Kalkül für Gleichheitsbeweise, welche typischerweise bei der Verifikation funktionaler Programme auftreten. Der Auswertungskalkül ist die vollautomatische Beweiskomponente des VeriFun-Systems und somit zu einem wesentlichen Teil für die Beweisautomatisierung verantwortlich.


Abstract auf Englisch:

This PhD thesis describes the symbolic evaluation calculus which has been develop in the context of the verification system VeriFun. This symbolic evaluation calculus is named a-calculus. The a-calculus is a logical calculus for solving equational problems, which typically occur during the verification of a functional program. It is the full-automatic proof-component of the VeriFun-System and thus responsible for the proof-automation of the VeriFun-System.

Dokument aufgenommen :2007-06-21
URL:http://elib.tu-darmstadt.de/diss/000831