Limit search to available items
Book Cover
E-book
Author International Symposium of Formal Methods Europe (23rd : 2019 : Porto, Portugal)

Title Formal methods -- the next 30 years : third World Congress, FM 2019, Porto, Portugal, October 7-11, 2019, Proceedings / Maurice H. ter Beek, Annabelle McIver, José N. Oliveira (eds.)
Published Cham, Switzerland : Springer, 2019

Copies

Description 1 online resource (xxi, 774 pages) : illustrations (some color)
Series Lecture notes in computer science ; 11800
Formal methods
LNCS sublibrary. SL 2, Programming and software engineering
Lecture notes in computer science ; 11800.
LNCS sublibrary. SL 2, Programming and software engineering.
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
Summary This book constitutes the refereed proceedings of the 23rd Symposium on Formal Methods, FM 2019, held in Porto, Portugal, in the form of the Third World Congress on Formal Methods, in October 2019. The 44 full papers presented together with 3 invited presentations were carefully reviewed and selected from 129 submissions. The papers are organized in topical sections named: Invited Presentations; Verification; Synthesis Techniques; Concurrency; Model Checking Circus; Model Checking; Analysis Techniques; Specification Languages; Reasoning Techniques; Modelling Languages; Learning-Based Techniques and Applications; Refactoring and Reprogramming; I-Day Presentations. -- Provided by publisher
Notes International conference proceedings
Includes author index
Online resource; title from PDF title page (SpringerLink, viewed September 26, 2019)
Subject Formal methods (Computer science) -- Congresses
Formal methods (Computer science)
Genre/Form Electronic books
proceedings (reports)
Conference papers and proceedings
Conference papers and proceedings.
Actes de congrès.
Form Electronic book
Author Beek, Maurice H. ter, editor.
McIver, Annabelle, editor.
Oliveira, José N., editor.
ISBN 9783030309428
3030309428
Other Titles FM 2019