The table below lists papers already accepted for presentation at FM’19 events.


EventTitleAuthor(s)
FM 2019A Parametric Rely-guarantee Reasoning Framework for Concurrent Reactive SystemsYongwang Zhao, David Sanan, Fuyuan Zhang and Yang Liu
FM 2019A Provably Correct Floating-Point Implementation of a Point-in-Polygon AlgorithmMariano Moscato, Laura Titolo, Marco Antonio Feliu Gabaldon and Cesar Munoz
FM 2019APML: An Architecture Proof Modelling LanguageDiego Marmsoler and Genc Blakqori
FM 2019Abstract ExecutionDominic Steinhöfel and Reiner Hähnle
FM 2019Abstraction and Subsumption in Modular Verification of C ProgramsLennart Beringer and Andrew W. Appel
FM 2019An Axiomatic Approach to Liveness for Differential EquationsYong Kiam Tan and André Platzer
FM 2019Circus2CSP: a Tool for Model-Checking Circus using FDRArtur Gomes and Andrew Butterfield
FM 2019Compositional verification of concurrent systems combining divbranching and strong bisimulationsFrédéric Lang, Radu Mateescu and Franco Mazzanti
FM 2019Concolic Testing Heap-Manipulating ProgramsLong H. Pham, Quang Loc Le, Quoc-Sang Phan and Jun Sun
FM 2019Controlling Large Boolean Networks with Temporary and Permanent PerturbationsCui Su, Soumya Paul and Jun Pang
FM 2019Counterexample-Driven Synthesis for Probabilistic Program SketchesMilan Ceska, Christian Dehnert, Sebastian Junges and Joost-Pieter Katoen
FM 2019Embedding High-Level Formal Specifications into ApplicationsPhilipp Koerner, Jens Bendisposto, Jannik Dunkelau, Sebastian Krings and Michael Leuschel
FM 2019Equilibria-based Probabilistic Model Checking for Concurrent Stochastic GamesMarta Kwiatkowska, Gethin Norman, David Parker and Gabriel Santos
FM 2019Formal Semantics Extraction from Natural Language Specifications for ARMAnh V. Vu and Mizuhito Ogawa
FM 2019Formally Verified Roundoff Errors using SMT-based Certificates and SubdivisionsJoachim Bard, Heiko Becker and Eva Darulova
FM 2019From LTL to Unambiguous Büchi Automata via Disambiguation of Alternating AutomataSimon Jantsch, David Müller, Christel Baier and Joachim Klein
FM 2019GOSPEL - Providing OCaml with a Formal Specification LanguageArthur Charguéraud, Jean-Christophe Filliâtre, Cláudio Lourenço and Mário Pereira
FM 2019GR(1)*: GR(1) Specifications Extended with Existential GuaranteesGal Amram, Shahar Maoz and Or Pistiner
FM 2019Generic Partition Refinement and Weighted Tree AutomataHans-Peter Deifel, Stefan Milius, Lutz Schröder and Thorsten Wißmann
FM 2019Gray-box Monitoring of HyperpropertiesSandro Stucki, Cesar Sanchez, Gerardo Schneider and Borzoo Bonakdarpour
FM 2019How Hard is Finding Shortest Counter-Example Lassos in Model Checking?Rüdiger Ehlers
FM 2019IELE: A Rigorously Designed Language and Tool Ecosystem for the BlockchainTheodoros Kasampalis, Dwight Guth, Brandon Moore, Traian Florin Serbanuta, Yi Zhang, Daniele Filaretti, Virgil Serbanuta, Ralph Johnson and Grigore Rosu
FM 2019L*-Based Learning of Markov Decision ProcessesMartin Tappler, Bernhard K. Aichernig, Giovanni Bacci, Maria Eichlseder and Kim Guldstrand Larsen
FM 2019Learning Deterministic Variable Automata over Infinite AlphabetsSarai Sheinvald
FM 2019Local Consistency Check in Dataflow ModelsDina Irofti and Paul Dubrulle
FM 2019Mechanically Verifying the Fundamental Liveness Property of the Chord ProtocolJean-Paul Bodeveix, Julien Brunel, David Chemouil and Mamoun Filali-Amine
FM 2019On the Nature of Symbolic ExecutionFrank De Boer and Marcello Bonsangue
FM 2019Optimization and Synthesis of Railway Signaling Layout from Local Capacity SpecificationsBjørnar Luteberget, Christian Johansen and Martin Steffen
FM 2019Parallel Composition and Modular Verification of Periodic Components in Differential Dynamic LogicSimon Lunel, Stefan Mitsch, Benoît Boyer and Jean-Pierre Talpin
FM 2019Pegasus: A Framework for Sound Continuous Invariant GenerationAndrew Sogokon, Stefan Mitsch, Yong Kiam Tan, Katherine Cordwell and André Platzer
FM 2019Quantitative Verification of Numerical Stability for Kalman FiltersAlexandros Evangelidis and David Parker
FM 2019Reasoning Formally about Database Queries and UpdatesJon Hael Brenas, Rachid Echahed and Martin Strecker
FM 2019Service-Oriented Architecture and The Button ProblemSung-Shik Jongmans, Arjan Lamers and Marko Van Eekelen
FM 2019Star-Based Reachability Analysis of Deep Neural NetworksHoang-Dung Tran, Diego Manzanas Lopez, Patrick Musau, Xiao Dong Yang, Luan Nguyen, Weiming Xiang and Taylor T Johnson
FM 2019Static Analysis for Detecting High-Level Races in RTOS KernelsAbhishek Singh, Rekha R, Deepak D'Souza and Meenakshi D'Souza
FM 2019Towards a model-checker for CircusArtur Gomes and Andrew Butterfield
FM 2019Unification in Matching LogicAndrei Arusoaie and Dorel Lucanu
FM 2019Value-dependent information-flow security on weak memory modelsGraeme Smith, Nicholas Coughlin and Toby Murray
FM 2019Verifying Correctness of Persistent Concurrent Data StructuresJohn Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn and Heike Wehrheim
DS 2019Blockmania QED.Maria A Schett
DS 2019Data Types in Logic ProgrammingJoão Barbosa
DS 2019Delayed Hybrid SystemsErzana Berani Abdelwahab
DS 2019Discrete Polymorphism with Gradual TypingPedro Jorge Fernandes Ângelo
DS 2019Formal Verification of Autonomous Driving SystemsYuvaraj Selvaraj
DS 2019Passlab: A Password Security Tool for the Blue TeamSaul Johnson
DS 2019Provable cyber security for industrial control systemsTomas Kulik
DS 2019Robustness Verification of Support Vector MachinesMarco Zanella
DS 2019Static Analysis of Python ProgramsRaphaël Monat
DS 2019TBA (Invited Talk)Sung-Shik Jongmans
i-Day 2019Adopting Formal Methods in an Industrial Setting: the Railways CaseMaurice ter Beek
i-Day 2019Formal Conceptual Modelling: Industrial Application of Event-B to a Wayside Train Monitoring SystemRobert Eschbach
i-Day 2019Formal Methods Applicability on Space Applications Specification and Implementation using MORA-TSPDaniel Silveira
i-Day 2019Formal Models as Executable Prototypes and Interactive Requirements Documents (Invited Talk)Michael Leuschel
i-Day 2019Practical Application of SPARK to OpenUxASM. Antony Aiello
i-Day 2019Property-Driven Software AnalysisDavid Deharbe
i-Day 2019TBA (Invited Talk)Constance Heitmeyer
MPC 2019A Hierarchy of Monadic Effects for Program Verification using Equational ReasoningReynald Affeldt, David Nowak and Takafumi Saikawa
MPC 2019An Analysis of Repeated Graph SearchRoland Backhouse
MPC 2019Certification of Breadth-First Algorithms by ExtractionDominique Larchey-Wendling and Ralph Matthes
MPC 2019Completeness and Incompleteness of Synchronous Kleene AlgebraJana Wagemaker, Tobias Kappé, Jurriaan Rot, Marcello Bonsangue and Alexandra Silva
MPC 2019Cylindric Kleene Lattices for Program ConstructionBrijesh Dongol, Ian J. Hayes, Larissa Meinicke and Georg Struth
MPC 2019En Garde! Unguarded Iteration for Reversible Computation in the Delay MonadNiccolò Veltri and Robin Kaarsgaard
MPC 2019Experiments in Information Flow Analysis (invited paper)Annabelle McIver
MPC 2019Handling Local State with Global StateKoen Pauwels, Tom Schrijvers and Shin-Cheng Mu
MPC 2019How to Calculate with Nondeterministic FunctionsRichard Bird and Florian Rabe
MPC 2019Self-Certifying Railroad Diagrams, Or: How to Teach Nondeterministic Finite AutomataRalf Hinze
MPC 2019Setoid Type Theory --- A Syntactic TranslationThorsten Altenkirch, Simon Boulier, Ambrus Kaposi and Nicolas Tabareau
MPC 2019Shallow Embedding of Type Theory is Morally CorrectAmbrus Kaposi, András Kovács and Nicolai Kraus
MPC 2019System F in Agda, for Fun and ProfitJames Chapman, Roman Kireev, Chad Nester and Philip Wadler
MPC 2019The Mean-Tempered Keyboard: Coding with Asymmetric Numeral SystemsJeremy Gibbons
MPC 2019Unraveling Recursion: Compiling an IR with Recursion to System FRoman Kireev, Chad Nester, Michael Peyton Jones, Philip Wadler, Vasilis Gkoumas and Kenneth MacKenzie
MPC 2019Verified Self-Explaining ComputationJan Stolarek and James Cheney
PPDP 201910 Years of the Higher-Order Model Checking Project (Invited Talk)Naoki Kobayashi
PPDP 2019TopHat: A formal foundation for task-oriented programmingTim Steenvoorden, Nico Naus and Markus Klinik
PPDP 2019An Adequate While-Language for Hybrid ComputationSergey Goncharov and Renato Neves
PPDP 2019Crumbling Abstract MachinesBeniamino Accattoli, Andrea Condoluci, Giulio Guerrieri and Claudio Sacerdoti Coen
PPDP 2019Exception Handling and Classical LogicSteffen van Bakel
PPDP 2019Exponential Elimination for Bicartesian Closed Categorical CombinatorsNachiappan Valliappan and Alejandro Russo
PPDP 2019Generic Encodings of Constructor Rewriting SystemsHoratiu Cirstea and Pierre-Etienne Moreau
PPDP 2019Inductive Theorem Proving in Non-terminating Rewriting Systems and Its Application to Program TransformationKentaro Kikuchi, Takahito Aoto and Isao Sasano
PPDP 2019Normalization by Evaluation for Call-by-Push-Value and Polarized Lambda-CalculusAndreas Abel and Christian Sattler
PPDP 2019Property-Based Testing via Proof ReconstructionRoberto Blanco, Dale Miller and Alberto Momigliano
PPDP 2019Sharing Equality is LinearBeniamino Accattoli, Andrea Condoluci and Claudio Sacerdoti Coen
PPDP 2019Smart Contracts as Authorized Production RulesBen Lippmeier, Amos Robinson and Andrae Muys
PPDP 2019TBC (Invited Talk)Amal Ahmed
RV 2019A Formally Verified Monitor for Metric First-Order Temporal LogicJoshua Schneider, David Basin, Srdjan Krstic and Dmitriy Traytel
RV 2019Accelerated Learning of Predictive Runtime Monitors for Rare FailureReza Babaee, Vijay Ganesh and Sean Sedwards
RV 2019AllenRV: an extensible monitor for multiple complex specifications with high reactivityNic Volanschi and Bernard Serpette
RV 2019An Extension of LTL with Rules and its Application to Runtime VerificationKlaus Havelund and Doron Peled
RV 2019Can we Verify GDPR Compliance? (Invited Talk)David Basin
RV 2019Challenges and opportunities in design and operation of intelligent cyber-physical system (Invited Talk)Akshay Rajhans
RV 2019Comparing Controlled System Synthesis and Suppression EnforcementIan Cassar, Luca Aceto, Adrian Francalanza and Anna Ingolfsdottir
RV 2019Decentralized Stream Runtime VerificationLuis Miguel Danielsson and Cesar Sanchez
RV 2019Efficient Detection and Quantification of Timing Leaks with Neural NetworksSaeid Tizpaz-Niari, Pavol Cerny, Sriram Sankaranarayanan and Ashutosh Trivedi
RV 2019FastCFI: Real-Time Control Flow Integrity using FPGA without Code InstrumentationLang Feng, Jeff Huang, Jiang Hu and Abhijith Reddy
RV 2019Monitorability Over Unreliable ChannelsSean Kauffman, Klaus Havelund and Sebastian Fischmeister
RV 2019Neural Predictive MonitoringLuca Bortolussi, Francesca Cairoli, Nicola Paoletti, Scott Smolka and Scott Stoller
RV 2019NuRV: a nuXmv Extension for Runtime VerificationAlessandro Cimatti, Chun Tian and Stefano Tonetta
RV 2019Overhead-aware deployment of runtime monitorsTeng Zhang, Gregory Eakman, Insup Lee and Oleg Sokolsky
RV 2019Predictive Runtime Monitoring for Linear Stochastic Systems and Applications to Geofence Enforcement for UAVsHansol Yoon, Yi Chou, Xin Chen, Eric Frew and Sriram Sankaranarayanan
RV 2019Reactive Control Meets Runtime Verification: A Case Study of NavigationDogan Ulus and Calin Belta
RV 2019Runtime Verification For Timed Event Streams With Partial InformationMartin Leucker, Cesar Sanchez, Torben Scheffel, Malte Schmitz and Daniel Thoma
RV 2019Shape Expressions for Specifying and Extracting Signal FeaturesDejan Nickovic, Xin Qin, Thomas Ferrère, Cristinel Mateis and Jyotirmoy Deshmukh
RV 2019TBA (Invited Talk)Sanjit A. Seshia
TAP 2019Coverage-Based Testing with Symbolic Transition SystemsPetra van den Bos and Jan Tretmans
TAP 2019Extracting Unverified Program Parts from Software Verification Runs (Keynote Talk)Heike Wehrheim
TAP 2019Learning Communicating State MachinesAlexandre Petrenko and Florent Avellaneda
TAP 2019Predicting and Testing Latencies with Deep Learning: an IoT Case StudyBernhard K. Aichernig, Franz Pernkopf, Richard Schumi and Andreas Wurm
TAP 2019Proving a Non-Blocking Algorithm for Process Renaming with TLA+Aurélie Hurault and Philippe Queinnec
TAP 2019Repairing Timed Automata Clock Guards through Abstraction and TestingÉtienne André, Paolo Arcaini, Angelo Gargantini and Marco Radavelli
TAP 2019RoboStar technology - Testing in Robotics Using Process Algebra (Invited TuTorial)Ana Cavalcanti