Formal Methods – The Next 30 Years: Third World Congress, FM 2019, Porto, Portugal, October 7–11, 2019, Proceedings

Description

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. Front Matter ....Pages i-xxi Front Matter ....Pages 1-1 The Human in Formal Methods (Shriram Krishnamurthi, Tim Nelson)....Pages 3-10 Successes in Deployed Verified Software (and Insights on Key Social Factors) (June Andronick)....Pages 11-17 Front Matter ....Pages 19-19 Provably Correct Floating-Point Implementation of a Point-in-Polygon Algorithm (Mariano M. Moscato, Laura Titolo, Marco A. Feliú, César A. Muñoz)....Pages 21-37 Formally Verified Roundoff Errors Using SMT-based Certificates and Subdivisions (Joachim Bard, Heiko Becker, Eva Darulova)....Pages 38-44 Mechanically Verifying the Fundamental Liveness Property of the Chord Protocol (Jean-Paul Bodeveix, Julien Brunel, David Chemouil, Mamoun Filali)....Pages 45-63 On the Nature of Symbolic Execution (Frank S. de Boer, Marcello Bonsangue)....Pages 64-80 Front Matter ....Pages 81-81 GR(1)*: GR(1) Specifications Extended with Existential Guarantees (Gal Amram, Shahar Maoz, Or Pistiner)....Pages 83-100 Counterexample-Driven Synthesis for Probabilistic Program Sketches (Milan Češka, Christian Hensel, Sebastian Junges, Joost-Pieter Katoen)....Pages 101-120 Synthesis of Railway Signaling Layout from Local Capacity Specifications (Bjørnar Luteberget, Christian Johansen, Martin Steffen)....Pages 121-137 Pegasus: A Framework for Sound Continuous Invariant Generation (Andrew Sogokon, Stefan Mitsch, Yong Kiam Tan, Katherine Cordwell, André Platzer)....Pages 138-157 Front Matter ....Pages 159-159 A Parametric Rely-Guarantee Reasoning Framework for Concurrent Reactive Systems (Yongwang Zhao, David Sanán, Fuyuan Zhang, Yang Liu)....Pages 161-178 Verifying Correctness of Persistent Concurrent Data Structures (John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim)....Pages 179-195 Compositional Verification of Concurrent Systems by Combining Bisimulations (Frédéric Lang, Radu Mateescu, Franco Mazzanti)....Pages 196-213 Front Matter ....Pages 215-215 Towards a Model-Checker for Circus (Artur Oliveira Gomes, Andrew Butterfield)....Pages 217-234 Circus2CSP: A Tool for Model-Checking Circus Using FDR (Artur Oliveira Gomes, Andrew Butterfield)....Pages 235-242 Front Matter ....Pages 243-243 How Hard Is Finding Shortest Counter-Example Lassos in Model Checking? (Rüdiger Ehlers)....Pages 245-261 From LTL to Unambiguous Büchi Automata via Disambiguation of Alternating Automata (Simon Jantsch, David Müller, Christel Baier, Joachim Klein)....Pages 262-279 Generic Partition Refinement and Weighted Tree Automata (Hans-Peter Deifel, Stefan Milius, Lutz Schröder, Thorsten Wißmann)....Pages 280-297 Equilibria-Based Probabilistic Model Checking for Concurrent Stochastic Games (Marta Kwiatkowska, Gethin Norman, David Parker, Gabriel Santos)....Pages 298-315 Front Matter ....Pages 317-317 Abstract Execution (Dominic Steinhöfel, Reiner Hähnle)....Pages 319-336 Static Analysis for Detecting High-Level Races in RTOS Kernels (Abhishek Singh, Rekha Pai, Deepak D’Souza, Meenakshi D’Souza)....Pages 337-353 Parallel Composition and Modular Verification of Computer Controlled Systems in Differential Dynamic Logic (Simon Lunel, Stefan Mitsch, Benoit Boyer, Jean-Pierre Talpin)....Pages 354-370 An Axiomatic Approach to Liveness for Differential Equations (Yong Kiam Tan, André Platzer)....Pages 371-388 Local Consistency Check in Synchronous Dataflow Models (Dina Irofti, Paul Dubrulle)....Pages 389-405 Gray-Box Monitoring of Hyperproperties (Sandro Stucki, César Sánchez, Gerardo Schneider, Borzoo Bonakdarpour)....Pages 406-424 Quantitative Verification of Numerical Stability for Kalman Filters (Alexandros Evangelidis, David Parker)....Pages 425-441 Concolic Testing Heap-Manipulating Programs (Long H. Pham, Quang Loc Le, Quoc-Sang Phan, Jun Sun)....Pages 442-461 Front Matter ....Pages 463-463 Formal Semantics Extraction from Natural Language Specifications for ARM (Anh V. Vu, Mizuhito Ogawa)....Pages 465-483 GOSPEL—Providing OCaml with a Formal Specification Language (Arthur Charguéraud, Jean-Christophe Filliâtre, Cláudio Lourenço, Mário Pereira)....Pages 484-501 Unification in Matching Logic (Andrei Arusoaie, Dorel Lucanu)....Pages 502-518 Embedding High-Level Formal Specifications into Applications (Philipp Körner, Jens Bendisposto, Jannik Dunkelau, Sebastian Krings, Michael Leuschel)....Pages 519-535 Front Matter ....Pages 537-537 Value-Dependent Information-Flow Security on Weak Memory Models (Graeme Smith, Nicholas Coughlin, Toby Murray)....Pages 539-555 Reasoning Formally About Database Queries and Updates (Jon Haël Brenas, Rachid Echahed, Martin Strecker)....Pages 556-572 Abstraction and Subsumption in Modular Verification of C Programs (Lennart Beringer, Andrew W. Appel)....Pages 573-590 Front Matter ....Pages 591-591 IELE: A Rigorously Designed Language and Tool Ecosystem for the Blockchain (Theodoros Kasampalis, Dwight Guth, Brandon Moore, Traian Florin Șerbănuță, Yi Zhang, Daniele Filaretti et al.)....Pages 593-610 APML: An Architecture Proof Modeling Language (Diego Marmsoler, Genc Blakqori)....Pages 611-630 Front Matter ....Pages 631-631 Learning Deterministic Variable Automata over Infinite Alphabets (Sarai Sheinvald)....Pages 633-650 \(L^*\)-Based Learning of Markov Decision Processes (Martin Tappler, Bernhard K. Aichernig, Giovanni Bacci, Maria Eichlseder, Kim G. Larsen)....Pages 651-669 Star-Based Reachability Analysis of Deep Neural Networks (Hoang-Dung Tran, Diago Manzanas Lopez, Patrick Musau, Xiaodong Yang, Luan Viet Nguyen, Weiming Xiang et al.)....Pages 670-686 Front Matter ....Pages 687-687 SOA and the Button Problem (Sung-Shik Jongmans, Arjan Lamers, Marko van Eekelen)....Pages 689-706 Controlling Large Boolean Networks with Temporary and Permanent Perturbations (Cui Su, Soumya Paul, Jun Pang)....Pages 707-724 Front Matter ....Pages 725-725 Formal Methods Applicability on Space Applications Specification and Implementation Using MORA-TSP (Daniel Silveira, Andreas Jung, Marcel Verhoef, Tiago Jorge)....Pages 727-737 Industrial Application of Event-B to a Wayside Train Monitoring System: Formal Conceptual Data Analysis (Robert Eschbach)....Pages 738-745 Property-Driven Software Analysis (Mathieu Comptier, David Déharbe, Paulin Fournier, Julien Molinero-Perez)....Pages 746-750 Practical Application of SPARK to OpenUxAS (M. Anthony Aiello, Claire Dross, Patrick Rogers, Laura Humphrey, James Hamil)....Pages 751-761 Adopting Formal Methods in an Industrial Setting: The Railways Case (Maurice H. ter Beek, Arne Borälv, Alessandro Fantechi, Alessio Ferrari, Stefania Gnesi, Christer Löfving et al.)....Pages 762-772 Back Matter ....Pages 773-774