Papers on our work using PVS

Fast Links:

Fault-Tolerance Hardware Verification Reflection

Compiler Verification Program Transformation Semantics of Programming Languages

• H. Pfeifer, F. von Henke
  Modular Formal Analysis of the Central Guardian in the Time-Triggered Architecture
  23rd International Conference on Computer Safety, Reliability and Security (SAFECOMP)
  Potsdam, Germany, September 21-24, 2004
  

• H. Pfeifer, F. von Henke
  Formal Analysis for Dependability Properties: the Time-Triggered Architecture Example
  8th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA 2001)
  Antibes Juan-les-pins, France, October 15-18, 2001
  

• H. Pfeifer
  Formal Verification of the TTP Group Membership Algorithm
  IFIP TC6/WG6.1 International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE XIII) and Protocol Specification, Testing and Verification (PSTV XX), FORTE/PSTV 2000
  Pisa, Italy, October, 2000

• H. Pfeifer, D. Schwier, F. W. von Henke
  Formal Verification for Time-Triggered Clock Synchronization
  Proc. Dependable Computing for Critical Applications (DCCA) 7
  San Jose, CA, 6-8 Jan. 1999.

• D. Schwier, F.W. von Henke
  Mechanical Verification of Clock Synchronization Algorithms
  Proc. FTRTFT'98, 5th Intl. Symp. Formal Techniques in Real-Time Fault-Tolerant Systems
  Springer LNCS 1486, Sept. 1998

• A. Dold, F. W. von Henke, V. Vialard, W. Goerigk
  A Mechanically Verified Compiling Specification for a Realistic Compiler
  Technical Report UIB 03-02, Universität Ulm, Fakultät für Informatik, Dec. 2002
  

• A. Dold, V. Vialard
  A Mechanically Verified Compiling Specification for a Lisp Compiler
  Proceedings of FSTTCS 2001, December 13-15, Bangalore, India.

• 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.
  

• Axel Dold, Vincent Vialard
  Formal Verification of a Compiler Back-end Generic Checker Program
  Proc. of 3rd Int. Conference Perspectives of System Informatics (PSI'99).
  Springer LNCS 1755.

• A. Dold, F. W. von Henke, H. Pfeifer, H. Rueß
  Formal Verification of Transformations for Peephole Optimization
  Proc. of FME'97, Springer LNCS 1313, pp. 459 - 472, September 1997.

• 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, Dec. 1995
  Note: This report is superseded by the FME'97 paper, see above.

• H. Rueß
  Hierarchical Verification of Two-Dimensional High-Speed Multiplication in PVS: A Case Study
  Proc. of FMCAD'96, Springer LNCS 1166, pp. 79-93, Nov. 1996, Palo Alto, CA

• H. Rueß, N. Shankar, and M. Srivas
  Modular Verification of SRT Division
  Proc. of CAV'96, Springer LNCS 1102, pp. 123-134, July 1996, New Brunswick, NJ

• D. Cyrluk, O. Möller, H. Rueß
  An Efficient Decision Procedure for a Theory of Fixed-Sized Bitvectors with Composition and Extraction
  Technical report UIB-96-8, Universität Ulm, Fakultät für Informatik, Dec. 1996

• D. Cyrluk, O. Möller, H. Rueß
  An Efficient Decision Procedure for the Theory of Fixed-Sized Bitvectors
  Proc. CAV'97, Springer LNCS 1254, pp. 60-71.

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

• 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
  Representing, Verifying and Applying Software Development Steps using the PVS System
  Proc. of AMAST'95, Springer LNCS 936, pp. 431-445, Montreal, 1995.

Semantics of Programming Languages

• 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
  Revised version as of Oct. 1997:
  Mechanizing Domain Theory

• 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
  Revised version as of July 1997:
  Guided Tour Through a Mechanized Semantics of Simple Imperative Programming Constructs

Reflection

• F. W. von Henke, S. Pfab, H. Pfeifer, H. Rueß
  Case Studies in Meta-Level Theorem Proving
  Proc. Intl. Conf. on Theorem Proving in Higher Order Logics
  Springer LNCS, Vol. 1479, pp. 461-478, Sept. 1998