TU Darmstadt / ULB / TUprints

Symbolische Auswertung und Heuristiken zur Verifikation funktionaler Programme

Schweitzer, Dirk Stephan (2007)
Symbolische Auswertung und Heuristiken zur Verifikation funktionaler Programme.
Technische Universität Darmstadt
Ph.D. Thesis, Primary publication

[img]
Preview
PDF
diss-druck.pdf
Copyright Information: In Copyright.

Download (2MB) | Preview
Item Type: Ph.D. Thesis
Type of entry: Primary publication
Title: Symbolische Auswertung und Heuristiken zur Verifikation funktionaler Programme
Language: German
Referees: Walther, Prof.Dr. Christroph ; Giesl, Prof.Dr. Jürgen
Advisors: Walther, Prof.Dr. Christroph
Date: 21 June 2007
Place of Publication: Darmstadt
Date of oral examination: 25 January 2007
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
URN: urn:nbn:de:tuda-tuprints-8311
Classification DDC: 000 Generalities, computers, information > 004 Computer science
Divisions: 20 Department of Computer Science
Date Deposited: 17 Oct 2008 09:22
Last Modified: 08 Jul 2020 22:58
URI: https://tuprints.ulb.tu-darmstadt.de/id/eprint/831
PPN:
Export:
Actions (login required)
View Item View Item