Provably Correct Systems

Foreword.- Preface.- Part I: Historic Account.- ProCoS: How It All Began - As Seen from Denmark.- Part II: Hybrid Systems .- Constraint-Solving Techniques for the Analysis of Probabilistic Hybrid Systems.- MARS: A Tool chain for Modelling, Analysis and Verification of Hybrid Systems.- Part III: Correctness of Concurrent Algorithms .- A Proof Method for Linearizability on TSO Architectures.- Part IV: Interfaces and Linking .- Linking Discrete and Continuous Models, Applied to Traffic Manoeuvres.- Towards Interface-Driven Design of Evolving Component-Based Architectures.- Part V: Automatic Verification .- Computing Verified Machine Address Bounds during Symbolic Exploration of Code.- Engineering a Formal, Executable x86 ISA Simulator for Software Verification.- Advances in Connection-Based Automated Theorem Proving.- Part VI: Run-Time Assertion Checking .- Run-Time Deadlock Detection.- In-Circuit Assertions and Exceptions for Reconfigurable Hardware Design.- Part VII: Formal and Semi-Formal Methods.- From ProCoS to Space and Mental Models - a Survey of Combing Formal and Semi-Formal Methods.- Part VIII: Web-Supported Communities in Science .- Provably Correct Systems: Community, Connections and Citations.