|
Title |
Authors |
Date |
Abstract |
Docu- ment |
Ref |
|
1999 | | | | |
|
Generic Compilation Schemes for Simple Programming Constructs
|
A.Dold
F.v.Henke
H.Pfeifer
H.Ruess
|
01/99
UIB 96-12
revised |
 |
 |
|
| Formalization of ComLisp and SIL |
A.Dold
|
01/99
Verifix Report
ULM 19.1 |
|
|
|
| Local Verification of Parametrized Compilation Rules in a Limited Resource Environment |
V.Vialard
|
01/99
Verifix Report
ULM 22.1 |
|
|
|
| Mechanizing Domain Theory |
F.Bartels
H.Pfeifer
F.v.Henke
H.Ruess
|
01/99
submitted |
|
|
|
|
|
The Verifix Approach Towards the Construction of Correct Compilers
|
W.Zimmermann
A.Heberle
W.Goerigk
|
02/99 |
|
|
|
|
| An Exercise in Compiler Verification Revisited --
Preserving Partial Correctness
|
A.Wolf
|
02/99
Verifix Report
CAU 6.1 |
|
|
|
| The Adequacy of a Loop's Definition |
A.Wolf
|
02/99
Verifix Report
CAU 6.2 |
|
|
|
|
Formal Verification of a Compiler-Backend Generic Checker Program
|
A.Dold
V.Vialard
|
02/99
submitted |
|
|
|
|
1998 | | | | |
| Efficient Abstract Interpretation of Formal
Specifications and Its Interrelationship with
Theorem Proving |
S.Pfab |
1998
Masters Thesis
Ulm |
|
|
|
| Formale Verifikation des DLX RISC-Prozessors: Eine Fallstudie
basierend auf abstrakten Zustandsmaschinen |
M.Stegmüller |
1998
Masters Thesis
ULM |
|
|
|
| Solving Bit-Vector Equations -
A Decision Procedure for Hardware Verification |
O.Möller |
1998
Masters Thesis
ULM |
|
|
|
|
Korrektheit der Daten- und Operationsverfeinerung für eine
applikative Sprache mit automatischer Speicherbereinigung
|
D.Michelsen |
1998
Masters Thesis
CAU |
|
|
|
|
Verifikation der Codegenerierung im Verifix-Projekt:
Prädikattransformer und Erhaltung partieller Korrektheit |
J.Ruehle |
1998
Masters Thesis
CAU |
| |
|
| The Formal Specification of IS |
A.Heberle
D.Heuzeroth
|
04/98
Verifix Report
UKA 2 revised |
|
|
|
| Correct Compilation of a While-Language with Parameterless Recursive Procedures |
T.Gaul
W.Goerigk
A.Heberle
U.Hoffmann
W.Zimmermann
|
06/98 |
|
|
|
| Codeerzeugung aus Abhängigkeitsgraphen |
B.Boesler |
06/98
Masters Thesis
UKA |
|
|
|
| Spezifikation und Verifikation von standardisierten
Transformationen am Beispiel der Übersetzung der
imperativen Sprache IS |
D.Heuzeroth |
08/98
Masters Thesis
UKA |
|
|
|
| An ASM Specification of the Operational Semantics od MIS |
T.Gaul
A.Heberle
D.Heuzeroth
W.Zimmermann
|
10/98
Verifix Report
UKA 3 Revised |
|
|
|
| Generische ASM Transformationen |
A.Merke |
11/98
Studienarbeit
UKA |
|
|
|
| Syntax einer Sprache zur textuellen Repräsentation
von Graphen |
A.Heberle
T.Gaul
|
1998 |
|
|
|
| The Compiling Specification from
ComLisp to Executable Machine Code |
W.Goerigk
U.Hoffmann
|
1998
CAU-TR Nr.9713 |
|
|
|
| Compiling ComLisp to Executable Machine Code:
Compiler Construction |
W.Goerigk
U.Hoffmann
|
1998
CAU-TR Nr.9812 |
|
|
|
| Correct Compiler Construction in PVS |
A.Dold
|
1998
Verifix Report
ULM 20.1 |
|
|
|
|
1997 | | | | |
| Denotational Semantics for ComLisp and SIL |
W.Goerigk
| 1997
Verifix Report
CAU 2.8 |
|
|
|
| Names, Types, and Static Semantic Analysis |
A.Heberle
S.Glesner
W.Löwe
|
06/97
UKA-TR
Nr.13/97 |
|
|
|
| Generating Semantic Analysis Using Constraint
Programming |
S.Glesner
A.Heberle
W.Löwe
|
06/97
UKA-TR
Nr. 15/97 |
|
|
|
| An Abstract State Machine for Java Byte Code |
T.Gaul
W.Zimmermann
|
12/97
Verifix Report
UKA 12 |
|
|
|
|
Algebraische Spezifikation eines generischen Integer-Datentyps
|
A.Heberle
D.Heuzeroth |
12/97
Verifix Report
UKA 14 |
|
|
|
|
1996 | | | | |
|
Simple code-generation for MIS to DEC-Alpha processor
|
T.Gaul |
04/96
Verifix Report
UKA 5 |
|
|
|
|
Specification and Verification of Compiler Frontend Tasks:
Semantic Analysis
|
A.Heberle
W.Zimmermann
G.Goos
|
04/96
Verifix Report
UKA 7 |
|
|
|
|
Verifiziertes Codeerzeugungsschema für die DEC-Alpha
Prozessor-Familie
|
T.Gaul A.Lange |
08/96
Verifix Report
UKA 13 |
|
|
|
| Supporting Refinement Calculus Proofs in PVS |
H.Pfeifer
A.Dold
F.v.Henke
H.Ruess
|
1996
Verifix Report
ULM 3.1 |
|
|
|
|
Representing the Alpha Processor Family using PVS
|
A.Dold
|
1996
Verifix Report
ULM 4.1 |
|
|
|
|
A Formal Representation of Abstract State Machines using PVS
|
A.Dold
|
1996
Verifix Report
ULM 6.2 |
|
|
|
|
Formal Specification of the Transputer Instruction Set in PVS
|
H.Pfeifer
A.Dold
F.v.Henke
H.Ruess
|
1996
Verifix Report
ULM 8.2 |
|
|
|
|
A Formalization of the Normalform Approach to Compilation
|
A.Dold
|
1996
Verifix Report
ULM 9.1 |
|
|
|
|
Modelling abstract views on the Transputer in PVS
|
H.Pfeifer
A.Dold
F.v.Henke
H.Ruess
|
1996
Verifix Report
ULM 13.1 |
|
|
|
|
Formalization and Verification of Code Generation Rules
|
A.Dold
|
09/96
Verifix Report
ULM 16.1 |
|
|
|
| The Compiler Implementation Language ComLisp |
W.Goerigk
U.Hoffmann
| 1996
Verifix Report
CAU 1.7 |
|
|
|
|
An Exercise in Program Verification: The ACL2 Correctness
Proof of a Simple Theorem Prover
|
W.Goerigk
| 1996
Verifix Report
CAU 2.4 |
|
|
|
|
Erhaltung partieller Korrektheit bei beschränkten
Maschinenressourcen. -- Eine Beweisskizze --
|
W.Goerigk
M.M.Olm
|
1996
Verifix Report
CAU 2.5 |
|
|
|
|
Three Views on Preservation of Partial Correctness
|
M.M.Olm
|
10/96
Verifix Report
CAU 5.1 |
|
|
|
| Bechmarking code-generation for IS to DEC-Alpha |
T.Gaul
|
11/96
Verifix Report
UKA 11 |
|
|
|
| Formalizing Fixed-Point Theory in PVS |
F. Bartels
A.Dold
F.v.Henke
H.Pfeifer
H.Ruess
|
1996
UIB 96-10 |
|
|
|
|
Mechanized Semantics of Simple Imperative Programming Constructs
|
H.Pfeifer
A.Dold
F.v.Henke
H.Pfeifer
H.Ruess
|
1996
UIB 96-11 |
|
|
|
|
1995 | | | |
| Transputer State and Instruction Set
Specification and Initial Boot Protocol |
W.Goerigk
| 1995
Verifix Report
CAU 2.1 |
|
|
|
| Definition of the Language IS |
A.Heberle
W.Zimmermann et-al
|
06/95
Verifix Report
UKA 1 |
|
|
|
|
An Abstract State Machine Specification for the DEC-Alpha
processor
|
T.Gaul
W.Zimmermann |
06/95
Verifix Report
UKA 4 |
|
|
|
