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)
    • Formally Verified Software in the Real World (restricted)
    • Formal Methods in Dependable Systems Engineering (local copy)
    • The Development and Deployment of Formal Methods in the UK (local copy)
    • A manifesto for applicable formal methods (local copy)
    • Demonstration Examples
  • Logic, Checking, and Proving (4 on 1)
    • Teaching the Formalization of Mathematical Theories and Algorithms via the Automatic Checking of Finite Models (local copy)
    • Demonstration Examples
• Specifying and Verifying Sequential Programs
  • Specifying and Verifying Programs (4 on 1)
    • Assigning Meanings to Programs (restricted)
    • An Axiomatic Basis for Computer Programming (restricted)
    • Demonstration Examples
• Specifying and Verifying Java Programs
  • The Java Modeling Language: Part 1 (4 on 1)
    • Behavioral Interface Specification Languages (restricted)
    • Specification and Verification: The Spec# Experience (restricted)
    • The Frama-C Software Analysis Platform (restricted)
    • Demonstration Examples
  • Extended Static Checking with ESC/Java 2 (4 on 1)
    • Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2 (local copy)
    • Satisfiability Modulo Theories: Introduction and Applications (restricted)
    • Demonstration Examples
  • 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)
    • Java Automated Deductive Verification in Practice: Lessons from Industrial Proof-Based Projects (restricted)
    • Demonstration Examples
• Specifying and Verifying Concurrent Systems
  • Modeling Concurrent Systems (4 on 1)
  • Specifying and Verifying System Properties (4 on 1)
    • Proving Safety and Liveness of Practical Distributed Systems (restricted)
    • 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