Linked e-resources
Details
Table of Contents
Intro; Preface; Organization; Formal Methods for Security Functionality and for Secure Functionality (Invited Presentation); Contents; Invited Presentations; The Human in Formal Methods; 1 Humans and Formal Methods; 2 User Experience; 3 Education; 3.1 A Design Recipe for Writing Specifications; 3.2 Tools; 4 Conclusion; References; Successes in Deployed Verified Software (and Insights on Key Social Factors); 1 The Dream; 2 Successes in Deployed Verified Software; 3 Insights on Key Social Factors; References; Verification
Provably Correct Floating-Point Implementation of a Point-in-Polygon Algorithm1 Introduction; 2 The Winding Number Algorithm; 3 Program Transformation to Avoid Unstable Tests; 4 Test-Stable Version of the Winding Number; 5 Verification Approach; 6 Related Work; 7 Conclusion; References; Formally Verified Roundoff Errors Using SMT-based Certificates and Subdivisions; 1 Introduction; 2 Extensions to FloVer; 3 Experiments; References; Mechanically Verifying the Fundamental Liveness Property of the Chord Protocol; 1 Introduction; 2 The Chord Protocol; 2.1 Network Structure; 2.1.1 Identifier Space
2.1.2 Chord Network2.2 Chord Operations; 2.2.1 Formal Model; 2.2.2 Model-Specific State Variables; 2.2.3 Events; 2.3 Proof Engineering; 3 Chord Correctness; 3.1 Generic Properties; 3.2 Chord Properties; 3.2.1 Chord Invariants; 3.2.2 Always-True Properties; 4 Phase-Based Convergence Proof; 4.1 Reaching MS1: Rectifying and prdc in Members; 4.2 Reaching MS2: The First Successor Is a Member; 4.3 Reaching MS3: Stabilizing only Includes Members; 4.4 Reaching MS4: prdc Is the Inverse of bestSucc and the Rectifying and Stabilizing Sets of Each Node Are Empty
4.5 Reaching MS5: The Tail of the Successor List of Each Node Is Equal to the Successor List of Its First Successor4.6 Reaching the Ideal State; 5 Related Work; 6 Conclusion; References; On the Nature of Symbolic Execution; 1 Introduction; 2 Basic Symbolic Execution; 3 Recursion; 4 Object Orientation; 5 Arrays, Multithreading, and Concurrent Objects; 6 Conclusion; References; Synthesis Techniques; GR(1)*: GR(1) Specifications Extended with Existential Guarantees; 1 Introduction; 1.1 Example: Lift Specification; 1.2 Related Work; 2 Preliminaries; 2.1 Game Structures and Strategies
2.2 Linear Temporal Logic and the GR(1) Fragment2.3 -calculus over Game Structures; 3 GR(1)*: Going Beyond LTL; 3.1 GR(1)* Formulas; 3.2 GR(1)* Winning Condition; 3.3 Inexpressibility of GR(1)* Winning Conditions in LTL; 4 Solving GR(1)* Games; 5 Strategy Construction; 5.1 Construction Discussion and Overview; 5.2 Detailed Construction; 6 Implementation and Preliminary Evaluation; 6.1 Setup; 6.2 Results; 7 Conclusion; References; Counterexample-Driven Synthesis for Probabilistic Program Sketches; 1 Introduction; 2 Preliminaries and Problem Statement; 3 CEGIS for Markov Chain Families
Provably Correct Floating-Point Implementation of a Point-in-Polygon Algorithm1 Introduction; 2 The Winding Number Algorithm; 3 Program Transformation to Avoid Unstable Tests; 4 Test-Stable Version of the Winding Number; 5 Verification Approach; 6 Related Work; 7 Conclusion; References; Formally Verified Roundoff Errors Using SMT-based Certificates and Subdivisions; 1 Introduction; 2 Extensions to FloVer; 3 Experiments; References; Mechanically Verifying the Fundamental Liveness Property of the Chord Protocol; 1 Introduction; 2 The Chord Protocol; 2.1 Network Structure; 2.1.1 Identifier Space
2.1.2 Chord Network2.2 Chord Operations; 2.2.1 Formal Model; 2.2.2 Model-Specific State Variables; 2.2.3 Events; 2.3 Proof Engineering; 3 Chord Correctness; 3.1 Generic Properties; 3.2 Chord Properties; 3.2.1 Chord Invariants; 3.2.2 Always-True Properties; 4 Phase-Based Convergence Proof; 4.1 Reaching MS1: Rectifying and prdc in Members; 4.2 Reaching MS2: The First Successor Is a Member; 4.3 Reaching MS3: Stabilizing only Includes Members; 4.4 Reaching MS4: prdc Is the Inverse of bestSucc and the Rectifying and Stabilizing Sets of Each Node Are Empty
4.5 Reaching MS5: The Tail of the Successor List of Each Node Is Equal to the Successor List of Its First Successor4.6 Reaching the Ideal State; 5 Related Work; 6 Conclusion; References; On the Nature of Symbolic Execution; 1 Introduction; 2 Basic Symbolic Execution; 3 Recursion; 4 Object Orientation; 5 Arrays, Multithreading, and Concurrent Objects; 6 Conclusion; References; Synthesis Techniques; GR(1)*: GR(1) Specifications Extended with Existential Guarantees; 1 Introduction; 1.1 Example: Lift Specification; 1.2 Related Work; 2 Preliminaries; 2.1 Game Structures and Strategies
2.2 Linear Temporal Logic and the GR(1) Fragment2.3 -calculus over Game Structures; 3 GR(1)*: Going Beyond LTL; 3.1 GR(1)* Formulas; 3.2 GR(1)* Winning Condition; 3.3 Inexpressibility of GR(1)* Winning Conditions in LTL; 4 Solving GR(1)* Games; 5 Strategy Construction; 5.1 Construction Discussion and Overview; 5.2 Detailed Construction; 6 Implementation and Preliminary Evaluation; 6.1 Setup; 6.2 Results; 7 Conclusion; References; Counterexample-Driven Synthesis for Probabilistic Program Sketches; 1 Introduction; 2 Preliminaries and Problem Statement; 3 CEGIS for Markov Chain Families