| 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 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 |
|
| 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: |
|
Print
Impressum
Sitemap
Search