Verifix at Kiel
Christian-Albrechts-Universität 
zu Kiel
 
           
  Home  
    Project Partners  
A. Dold, W. Goerigk, M. Müller-Olm, J. Rühle
Erhaltung partieller Korrektheit bei Maschinenressourcenbeschränkungen: Korrektheitsbeweis und Formalisierung in PVS
[Verifix/CAU-Ulm/2.3]
In Vorbereitung.


W. Goerigk
Denotational Semantics for ComLisp and SIL (DRAFT)
[Verifix/CAU/2.8]
Dezember 1997 (Stand: April 1998)


W. Goerigk
Transputer State, Instruction Set and Initial Boot Protocol (DRAFT)
[Verifix/CAU/2.1]
Juli 1995 (Stand: September 1996)


W. Goerigk
An Exercise in Program Verification: The ACL2 Correctness Proof of a Simple Theorem Prover Executable
[Verifix/CAU/2.4]
September 1996 (Stand: Dezember 1996)


W. Goerigk, U. Hoffmann
The Compiler Implementation Language ComLisp
[Verifix/CAU/1.7]
Juni 1995 (Stand: März 1996)


W. Goerigk, U. Hoffmann, H. Langmaack
Rigorous Compiler Implementation Correctness: How to Prove the Real Thing Correct
[Verifix/CAU/2.6]
Januar 1997 (Stand: Juni 1997)


W. Goerigk, Th. Meyer, H. Pfeifer, J. Rühle
Boot Loader Correctness: The Transputer Boot Program and its Correctness Proof in PVS
[Verifix/CAU-Ulm/2.2]
In Vorbereitung.


W. Goerigk, M. Müller-Olm
Erhaltung partieller Korrektheit bei beschränkten Maschinenressourcen.
- Eine Beweisskizze -
[Verifix/CAU/2.5]
Dezember 1996 (Stand: Dezember 1996)


U. Hoffmann
Über die korrekte Implementierung von Compilern
[Verifix/CAU/3.1]
März 1996 (Stand: Juni 1996)


U. Hoffmann
Überblick über die Übersetzung von der Compiler-Implementierungssprache ComLisp in den Maschinencode TC des Transputers
[Verifix/CAU/1.1]
In Vorbereitung.


U. Hoffmann
Die Übersetzerzwischensprache SIL
[Verifix/CAU/1.3]
In Vorbereitung.


U. Hoffmann
Die Übersetzerzwischensprache intermediateC
[Verifix/CAU/1.4]
In Vorbereitung.


U. Hoffmann
Die Assemblersprache TASM des Transputers
[Verifix/CAU/1.5]
In Vorbereitung.


U. Hoffmann
Die Übersetzung von Cint in den Assemblercode TASM des Transputer
[Verifix/CAU/1.6]
Februar 1996 (Stand: September 1996)


U. Hoffmann
Die Übersetzung von ComLisp in die Compiler-Zwischensprache SIL
[Verifix/CAU/1.8]
Juni 1996 (Stand: Juni 1996)


U. Hoffmann
Die Übersetzung von SIL nach Cint
[Verifix/CAU/1.9]
Juni 1996 (Stand: Juni 1996)


U. Hoffmann
Das Übersetzerprogramm von ComLisp nach SIL
[Verifix/CAU/1.10]
Juni 1996 (Stand: Oktober 1996)


U. Hoffmann, H. Pfeifer
Formalisierung der Übersetzung von Cint nach TASS und ihr mechanischer Korrektheitsbeweis
[Verifix/CAU-Ulm/1.1]
In Vorbereitung.


H. Langmaack
Softwareengineering zur Zertifizierung von Systemen: Spezifikations-, Implementierungs-, Übersetzerkorrektheit
[Verifix/CAU/4.1]
August 1996 (Stand: August 1996)


H. Langmaack
Ein Beitrag zu Goodenoughs und Gerharts Theorie des Softwaretestens und -verifizierens: Beziehungen zwischen starkem Übersetzertest und Übersetzerimplementierungsverifikation
[Verifix/CAU/4.1]
August 1996 (Stand: August 1996)


M. Müller-Olm
Three Views on Preservation of Partial Correctness
[Verifix/CAU/5.1]
Oktober 1996 (Stand: Oktober 1996)


Andreas Wolf
An Exercise in Compiler Verification Revisited - Preserving Partial Correctness
[Verifix/CAU/6.1]
Februar 1999 (Stand: Februar 1999)


Andreas Wolf
The Adequacy of a Loop's Definition
[Verifix/CAU/6.2]
Februar 1999 (Stand: Februar 1999)
 
 
 
  Staff  
    Publications  
   Technical Reports  
   Verifix-Reports  
    Workshops  
    Technicalities  
    Code Reviews  
   Contact