Dr. Axel Dold

	Axel Dold  Abtl. Künstliche Intelligenz  Universität Ulm  D-89069 Ulm
	(+49) 731 / 50 - 24117			(+49) 731 / 50 - 24119
	dold@ki.informatik.uni-ulm.de			O 27 / 422

• Formal Verification of Software,
• Formalization and Verification of Program Transformations,
• Formal Verification of Compilation Processes

• KORSO (Correct Software)
• Verifix (Verified Compilers)

• W. Zimmermann, A. Dold
  A Framework for Modelling the Semantics of Expression Evaluation with Abstract State Machines
  Proc. of the 9th International Workshop on Abstract State Machines (ASM 2003),
  Springer LNCS, to appear.

• A. Dold, V. Vialard
  A Mechanically Verified Bootstrap Compiler
  Proc. of Kolloquium Programmiersprachen und Grundlagen der Programmierung
  Technical report AIB-2001-11,
  RWTH Aachen, Department of Computer Science, December 2001.
  

• A. Dold, V. Vialard
  A Mechanically Verified Compiling Specification for a Lisp Compiler
  Proc. of the 21st Conference on
  Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2001),
  December 13-15, Bangalore, India.
  Springer LNCS 2245.
  

• A. Dold
  Formal Software Development using Generic Development Steps
  PhD thesis, Universität Ulm, 2000.

• A. Dold
  Formal Software Development using Generic Development Steps
  Proc. of the 11th Nordic Workshop on Programming Theory (NWPT'99 ),
  Uppsala, Sweden, October 6-8, 1999 (Abstract).
  

• A. Dold, V. Vialard
  Formal Verification of a Compiler Back-End Generic Checker Program
  Proceedings of the Andrei Ershov Third International Conference
  Perspectives of System Informatics (PSI'99),
  Novosibirsk, Akademgorodok, Russia, July 6 - 9, 1999.
  Springer LNCS 1755.
  

• A. Dold
  Software Development in PVS using Generic Development Steps
  In Generic Programming - International Seminar on Generic Programming
  Schloss Dagstuhl, April 27 - May 1, 1998, Selected Papers.
  Springer LNCS 1766, 2000.

• A. Dold, T. Gaul, V. Vialard, W. Zimmermann
  ASM-Based Mechanized Verification of Compiler Backends
  Proc. 5th International Workshop on Abstract State Machines,
  Magdeburg, Germany, September 21-22, 1998.
  

• A. Dold, T. Gaul, W. Zimmermann
  Mechanized Verification of Compiler Backends
  Proc. of the Internat. Workshop on Software Tools for Technology Transfer (STTT'98),
  Aalborg, Denmark, July 12-13, 1998.
  

• A. Dold, F. W. von Henke, H. Pfeifer, H. Rueß
  Formal Verification of Transformations for Peephole Optimization
  Proc. 4th International Symposium of Formal Methods Europe,
  Graz, Austria, September 15-19, 1997.
  Springer LNCS 1313.
  

• F. Bartels, A. Dold, F. W. v. Henke, H. Pfeifer, and H. Rueß
  Formalizing Fixed-Point Theory in PVS
  Technical report UIB 96-10, Universität Ulm, Fakultät für Informatik, Dec. 1996
  

• H. Pfeifer, A. Dold, F. W. v. Henke, and H. Rueß
  Mechanized Semantics of Imperative Programming Constructs
  Technical report UIB 96-11, Universität Ulm, Fakultät für Informatik, Dec. 1996
  

• A. Dold, F. W. von Henke, H. Pfeifer, H. Rueß
  Generic Compilation Schemes for Simple Programming Constructs
  Technical report UIB 96-12, Universität Ulm, Fakultät für Informatik, Dec. 1996
  (a revised version (Jan'99) is available here .)

• W. Goerigk, A. Dold, Th. Gaul, G. Goos, A. Heberle, F.W. von Henke, U. Hoffmann,
  H. Langmaack, H. Pfeifer, H. Rueß, and W. Zimmermann.
  Compiler Correctness and Implementation Verification: The Verifix Approach.
  In P. Fritzson (ed.) Proc. of the Poster Session of CC '96 - International Conference on Compiler Construction,
  IDA Technical Report LiTH-IDA-R-96-12, Linkøping University, Sweden, April 1996.
  

• A. Dold, F. W. von Henke, H. Pfeifer, H. Rueß
  A Generic Specification for Verifying Peephole Optimizations
  Technical report UIB 95-14, Universität Ulm, Fakultät für Informatik.

• A. Dold
  Representing, Verifying and Applying Software Development Steps using the PVS System
  Proc. of the 4th International Conference on Algebraic Methodology and Software Technology,
  AMAST'95, Montreal, 1995.
  Springer LNCS 936.

• F.W. von Henke, A. Dold , H. Rueß, D. Schwier, and M. Strecker
  Construction and Deduction Methods for the Formal Development of Software
  in KORSO: Methods, Languages, and Tools for the Construction of Correct Software
  Springer LNCS 1009, 1995.
  

• A. Dold
  Formalisierung schematischer Algorithmen (in German)
  Technical report UIB 94-10, Universität Ulm, Fakultät für Informatik, Jan. 1994.
• F.W. von Henke, A. Dold , H. Rueß, D. Schwier, and M. Strecker
  Construction and Deduction Methods for the Formal Development of Software
  Technical report UIB 94-09, Universität Ulm, Fakultät für Informatik.
• A. Dold
  Formalisierung schematischer Algorithmen
  in Arbeitstreffen Typtheorie: Zusammenfassung der Beiträge
  Technical report UIB 94-08, Universität Ulm, Fakultät für Informatik.
• Axel Dold
  Ginsberg's Bilatices and Nonmonotonic Consequence Operations
  Technical report, Master Thesis, Karlsruhe University (in German), 1992.

• Jürgen Dix, Axel Dold, Thomas Fuchß, and Martin Müller.
  Theorist und MVL: Erfahrungen und Hinweise im Umgang mit nichtmonotonen Beweissystemen.
  Technical report, Universität Karlsruhe, Fak. für Informatik,
  Institut für Logik, Komplexität und Deduktionssysteme, July 1990.

• Kolloquium Programmiersprachen und Grundlagen der Programmierung ,
  Hotel Paulushof, Rurberg, Eifel, October 7-11, 2001.
• Workshop on Engineering of Software Verification, Validation, and Certification, Kiel, June 26, 1998.
• Dagstuhl Seminar on Generic Programming, Schloß Dagstuhl, April 27 - May 1, 1998.