| 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 Abstract | Language |
|---|
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: |
|
Drucken
Impressum