Intro
Introduction
Organization
Contents - Part I
SpecifyThis
Bridging Gaps Between Program Specification Paradigms
SpecifyThis
Bridging Gaps Between Program Specification Paradigms
1 Introduction
2 Summary of Contributions
References
Deductive Verification Based Abstraction for Software Model Checking
1 Introduction
2 Overview of the Verification Approach
3 Deductive Verification and Frama-C
4 Model Checking and TLA
4.1 The TLA Framework
4.2 Translating Code and Contracts into TLA
5 Contracts as a Unifying Theory

5.1 An Abstract Contract Theory
5.2 Deductive Verification in the Abstract Contract Theory
5.3 Procedure-Modular Verification with TLA
5.4 Contract Based System Design
6 Preliminary Evaluation
6.1 Simple File Open-Close Example
6.2 Simplified Industrial Example
7 Conclusion
References
Abstraction in Deductive Verification: Model Fields and Model Methods
1 Introduction
2 Logical Encoding of Local Computations
3 Encoding Heap Access and Update-Previous and Related Work
3.1 Notation
3.2 Heaps as Maps
3.3 Arrays
3.4 Embedding in SMT

4 Model Fields and Model Methods
5 Simple Example
6 Using Model Methods
7 Encoding Model Methods
8 Contrast and Conclusion
References
A Hoare Logic with Regular Behavioral Specifications
1 Introduction
2 Motivation
3 Approach
3.1 Preliminaries and Notation
3.2 Regular Behavioral Specifications
3.3 Programs and Behavioral Correctness
3.4 Hoare Logic Proof Rules
4 Tool Support in SecC
4.1 Specification Syntax
4.2 Verification Engine
5 Case Studies
5.1 Case Study: Regular Expression Matching
5.2 Case-Study: VerifyThis Casino Challenge

5.3 Discussion
6 Related and Alternative Approaches
7 Conclusion
References
Specification-Based Monitoring in C++
1 Introduction
2 Related Work
3 Overview
4 The Specification Language
4.1 Events
4.2 A Simple State Machine
4.3 Some Alternative Monitors
4.4 Monitoring Events that Carry Data
4.5 Referring to the Past
4.6 A Complex Property
4.7 The Complete Grammar
5 Usage
6 Implementation
7 Experiment
7.1 Setting Up the Experiment
7.2 Result and Interpretation
8 Conclusion
A Visualization of Monitors
References

Specification and Verification with the TLA+ Trifecta: TLC, Apalache, and TLAPS
1 Introduction
2 Specifying Termination Detection
3 Verification by Model Checking and Theorem Proving
3.1 Finite-State Model Checking Using tlc
3.2 Bounded Model Checking with Apalache
3.3 Theorem Proving Using tlaps
4 Safra's Algorithm for Termination Detection
5 Analyzing Safra's Algorithm
5.1 Model Checking Correctness Properties
5.2 Safra's Algorithm Implements Termination Detection
5.3 Proving Correctness Using tlaps
6 Conclusion
References