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

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