TU Darmstadt / ULB / tuprints

Symbolische Auswertung und Heuristiken zur Verifikation funktionaler Programme

Schweitzer, Dirk Stephan :
Symbolische Auswertung und Heuristiken zur Verifikation funktionaler Programme.
[Online-Edition]
TU Darmstadt
[Ph.D. Thesis], (2007)

[img]
Preview
PDF
diss-druck.pdf
Available under Simple publication rights for ULB.

Download (2019Kb) | Preview
Item Type: Ph.D. Thesis
Title: Symbolische Auswertung und Heuristiken zur Verifikation funktionaler Programme
Language: German
Abstract:

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.

Alternative Abstract:
Alternative AbstractLanguage
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.English
Classification DDC: 000 Allgemeines, Informatik, Informationswissenschaft > 004 Informatik
Divisions: Fachbereich Informatik
Date Deposited: 17 Oct 2008 09:22
Last Modified: 07 Dec 2012 11:53
Official URL: http://elib.tu-darmstadt.de/diss/000831
URN: urn:nbn:de:tuda-tuprints-8311
License: Simple publication rights for ULB
Referees: Walther, Prof.Dr. Christroph and Giesl, Prof.Dr. Jürgen
Advisors: Walther, Prof.Dr. Christroph
Refereed: 25 January 2007
URI: http://tuprints.ulb.tu-darmstadt.de/id/eprint/831
Export:

Actions (login required)

View Item View Item