default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDFM 2019: Porto, Portugal
- Maurice H. ter Beek, Annabelle McIver, José N. Oliveira:
Formal Methods - The Next 30 Years - Third World Congress, FM 2019, Porto, Portugal, October 7-11, 2019, Proceedings. Lecture Notes in Computer Science 11800, Springer 2019, ISBN 978-3-030-30941-1
Invited Presentations
- Shriram Krishnamurthi
, Tim Nelson:
The Human in Formal Methods. 3-10 - June Andronick:
Successes in Deployed Verified Software (and Insights on Key Social Factors). 11-17
Verification
- Mariano M. Moscato, Laura Titolo, Marco A. Feliú, César A. Muñoz:
Provably Correct Floating-Point Implementation of a Point-in-Polygon Algorithm. 21-37 - Joachim Bard, Heiko Becker, Eva Darulova:
Formally Verified Roundoff Errors Using SMT-based Certificates and Subdivisions. 38-44 - Jean-Paul Bodeveix, Julien Brunel, David Chemouil, Mamoun Filali:
Mechanically Verifying the Fundamental Liveness Property of the Chord Protocol. 45-63 - Frank S. de Boer, Marcello M. Bonsangue:
On the Nature of Symbolic Execution. 64-80
Synthesis Techniques
- Gal Amram, Shahar Maoz, Or Pistiner:
GR(1)*: GR(1) Specifications Extended with Existential Guarantees. 83-100 - Milan Ceska, Christian Hensel, Sebastian Junges, Joost-Pieter Katoen:
Counterexample-Driven Synthesis for Probabilistic Program Sketches. 101-120 - Bjørnar Luteberget, Christian Johansen, Martin Steffen:
Synthesis of Railway Signaling Layout from Local Capacity Specifications. 121-137 - Andrew Sogokon, Stefan Mitsch, Yong Kiam Tan, Katherine Cordwell, André Platzer:
Pegasus: A Framework for Sound Continuous Invariant Generation. 138-157
Concurrency
- Yongwang Zhao, David Sanán, Fuyuan Zhang, Yang Liu:
A Parametric Rely-Guarantee Reasoning Framework for Concurrent Reactive Systems. 161-178 - John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim:
Verifying Correctness of Persistent Concurrent Data Structures. 179-195 - Frédéric Lang, Radu Mateescu, Franco Mazzanti:
Compositional Verification of Concurrent Systems by Combining Bisimulations. 196-213
Model Checking Circus
- Artur Oliveira Gomes, Andrew Butterfield:
Towards a Model-Checker for Circus. 217-234 - Artur Oliveira Gomes, Andrew Butterfield:
Circus2CSP: A Tool for Model-Checking Circus Using FDR. 235-242
Model Checking
- Rüdiger Ehlers:
How Hard Is Finding Shortest Counter-Example Lassos in Model Checking? 245-261 - Simon Jantsch, David Müller, Christel Baier, Joachim Klein:
From LTL to Unambiguous Büchi Automata via Disambiguation of Alternating Automata. 262-279 - Hans-Peter Deifel, Stefan Milius, Lutz Schröder, Thorsten Wißmann:
Generic Partition Refinement and Weighted Tree Automata. 280-297 - Marta Kwiatkowska, Gethin Norman, David Parker, Gabriel Santos:
Equilibria-Based Probabilistic Model Checking for Concurrent Stochastic Games. 298-315
Analysis Techniques
- Dominic Steinhöfel, Reiner Hähnle:
Abstract Execution. 319-336 - Abhishek Singh, Rekha R. Pai, Deepak D'Souza, Meenakshi D'Souza:
Static Analysis for Detecting High-Level Races in RTOS Kernels. 337-353 - Simon Lunel, Stefan Mitsch, Benoît Boyer, Jean-Pierre Talpin:
Parallel Composition and Modular Verification of Computer Controlled Systems in Differential Dynamic Logic. 354-370 - Yong Kiam Tan, André Platzer:
An Axiomatic Approach to Liveness for Differential Equations. 371-388 - Dina Irofti, Paul Dubrulle:
Local Consistency Check in Synchronous Dataflow Models. 389-405 - Sandro Stucki, César Sánchez, Gerardo Schneider, Borzoo Bonakdarpour:
Gray-Box Monitoring of Hyperproperties. 406-424 - Alexandros Evangelidis, David Parker:
Quantitative Verification of Numerical Stability for Kalman Filters. 425-441 - Long H. Pham, Quang Loc Le, Quoc-Sang Phan, Jun Sun:
Concolic Testing Heap-Manipulating Programs. 442-461
Specification Languages
- Anh V. Vu, Mizuhito Ogawa:
Formal Semantics Extraction from Natural Language Specifications for ARM. 465-483 - Arthur Charguéraud, Jean-Christophe Filliâtre, Cláudio Lourenço, Mário Pereira:
GOSPEL - Providing OCaml with a Formal Specification Language. 484-501 - Andrei Arusoaie, Dorel Lucanu:
Unification in Matching Logic. 502-518 - Philipp Körner, Jens Bendisposto, Jannik Dunkelau, Sebastian Krings, Michael Leuschel:
Embedding High-Level Formal Specifications into Applications. 519-535
Reasoning Techniques
- Graeme Smith, Nicholas Coughlin, Toby Murray:
Value-Dependent Information-Flow Security on Weak Memory Models. 539-555 - Jon Haël Brenas, Rachid Echahed, Martin Strecker:
Reasoning Formally About Database Queries and Updates. 556-572 - Lennart Beringer, Andrew W. Appel:
Abstraction and Subsumption in Modular Verification of C Programs. 573-590
Modelling Languages
- Theodoros Kasampalis, Dwight Guth, Brandon M. Moore, Traian-Florin Serbanuta, Yi Zhang, Daniele Filaretti, Virgil Nicolae Serbanuta, Ralph Johnson, Grigore Rosu:
IELE: A Rigorously Designed Language and Tool Ecosystem for the Blockchain. 593-610 - Diego Marmsoler, Genc Blakqori:
APML: An Architecture Proof Modeling Language. 611-630
Learning-Based Techniques and Applications
- Sarai Sheinvald:
Learning Deterministic Variable Automata over Infinite Alphabets. 633-650 - Martin Tappler, Bernhard K. Aichernig, Giovanni Bacci, Maria Eichlseder, Kim G. Larsen:
L*-Based Learning of Markov Decision Processes. 651-669 - Hoang-Dung Tran, Diego Manzanas Lopez, Patrick Musau, Xiaodong Yang, Luan Viet Nguyen, Weiming Xiang, Taylor T. Johnson:
Star-Based Reachability Analysis of Deep Neural Networks. 670-686
Refactoring and Reprogramming
- Sung-Shik Jongmans, Arjan Lamers, Marko C. J. D. van Eekelen:
SOA and the Button Problem. 689-706 - Cui Su, Soumya Paul, Jun Pang:
Controlling Large Boolean Networks with Temporary and Permanent Perturbations. 707-724
I-Day Presentations
- Daniel Silveira, Andreas Jung, Marcel Verhoef, Tiago Jorge:
Formal Methods Applicability on Space Applications Specification and Implementation Using MORA-TSP. 727-737 - Robert Eschbach:
Industrial Application of Event-B to a Wayside Train Monitoring System: Formal Conceptual Data Analysis. 738-745 - Mathieu Comptier, David Déharbe, Paulin Fournier, Julien Molinero Perez:
Property-Driven Software Analysis - (Extended Abstract). 746-750 - M. Anthony Aiello, Claire Dross, Patrick Rogers, Laura R. Humphrey, James Hamil:
Practical Application of SPARK to OpenUxAS. 751-761 - Maurice H. ter Beek, Arne Borälv, Alessandro Fantechi, Alessio Ferrari, Stefania Gnesi, Christer Löfving, Franco Mazzanti:
Adopting Formal Methods in an Industrial Setting: The Railways Case. 762-772
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2025-10-30 00:39 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
