Materials

• Computer Programs/Systems as Subject of Formal Reasoning
• Introduction (4 on 1)
• Fehler im System: der Traum von Software ohne Bugs (restricted)
• Retrospective: Hoare: An Axiomatic Basis for Computer Programming (restricted)
• Formal Methods: Practice and Experience (local copy)
• Demonstration Examples
• Logic and Proving (4 on 1)
• Demonstration Examples
• Specifying and Verifying Sequential Programs
• Specifying and Verifying Programs: Part 1 (4 on 1)
• An Axiomatic Basis for Computer Programming (restricted)
• linsearch3.zip
• Specifying and Verifying Programs: Part 2 (4 on 1)
• Computer-based Program Reasoning based on a Relational Semantics of Programs (local copy)
• Demonstration Examples
• Compositional Approach for Program Specification and Verification (Nikitchenko)
  • Syllabus
  • Compositional Approach to Program Formalization and Verification (methodological introduction)
    
  • Integrating Programming-Related Disciplines: Main Principles and Notions (restricted)
  • Basics of Intensionalized Data: Presets, Sets, and Nominats (restricted)
  • Developing Composition-Nominative Program Logics
  • Tables
  • Paper (restricted)
  • Compositional Methods of Program Verification
• Specifying and Verifying Java Programs
• The Java Modeling Language: Part 1 (4 on 1)
• Behavioral Interface Specification Languages
• Specification and Verification: The Spec# Experience (restricted)
• Extended Static Checking with ESC/Java 2 (4 on 1)
• Demonstration Examples
• Satisfiability Modulo Theories: Introduction and Applications (restricted)
• Verifying Java Programs with KeY (4 on 1)
• Demonstration Examples
• The Java Modeling Language: Part 2 (4 on 1)
• Proof of Correctness of Data Representations (restricted)
• Formal Verification of Object-Oriented Software (COST Action IC0701)
• Demonstration Examples
• Specifying and Verifying Concurrent Systems
• Modeling Concurrent Systems (4 on 1)
• Specifying and Verifying System Properties (4 on 1)
• Demonstration Examples
• Model-Checking Concurrent Systems (4 on 1)
• Abstrakte Kunst: Fehler finden durch Model Checker (restricted)
• Talking Model Checking Technology (restricted)
• Demonstration Examples

Restricted Area

The password to this area is handed out in class.