The table below lists all 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 César Muñoz
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 2019Alloy*: a general-purpose higher-order relational constraint solver (Journal First Track)Aleksandar Milicevic, Joseph P. Near, Eunsuk Kang and Daniel Jackson
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 2019Conditions of contracts for separating responsibilities in heterogeneous systems (Journal First Track)Jonas Westman and Mattias Nyberg
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 Methods for Security Functionality and for Secure Functionality (Invited Talk)Erik Poll
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, César Sánchez, 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 Roşu
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 2019Successes in Deployed Verified Software (and Insights on Key Social Factors) (Invited Talk)June Andronick
FM 2019The Human in Formal Methods (Invited Talk)Shriram Krishnamurthi
FM 2019Towards a model-checker for CircusArtur Gomes and Andrew Butterfield
FM 2019Unification in Matching LogicAndrei Arusoaie and Dorel Lucanu
FM 2019Unifying separation logic and region logic to allow interoperability (Journal First Track)Yuyan Bao, Gary T. Leavens and Gidon Ernst
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 2019Synthesising Monitors for Autonomous TrafficChristopher Bischopink
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 2019On the Role of Formal Methods in Assuring Autonomous Systems That Use Machine Learning (Invited Talk)Constance Heitmeyer
i-Day 2019Practical Application of SPARK to OpenUxASAnthony Aiello
i-Day 2019Property-Driven Software AnalysisDavid Déharbe
LOPSTR 2019A Certified Functional Nominal C-Unification AlgorithmMauricio Ayala-Rincon, Maribel Fernández, Gabriel Silva and Daniele Nantes-Sobrinho
LOPSTR 2019A General Framework for Static Cost Analysis of Parallel Logic ProgramsMaximiliano Klemen, Pedro Lopez-Garcia, John Gallagher, Jose F. Morales and Manuel Hermenegildo
LOPSTR 2019A Port Graph Rewriting Approach toRelational Database ModellingJanos Varga, Maribel Fernández and Bruno Pinaud
LOPSTR 2019An Integrated Approach to Assertion-Based Random Testing in PrologIgnacio Casso, Jose F. Morales and Manuel Hermenegildo
LOPSTR 2019An Optional Static Type System for PrologIsabel Wingen and Philipp Koerner
LOPSTR 2019Blockchain SuperoptimizerJulian Nagele and Maria Anna Schett
LOPSTR 2019Computing Abstract Distances in Logic ProgramsIgnacio Casso, Jose F. Morales, Pedro Lopez-Garcia and Manuel Hermenegildo
LOPSTR 2019Generalization-driven semantic clone detection in CLP (Extended Abstract)Wim Vanhoof and Gonzague Yernaux
LOPSTR 2019Incremental Analysis of Logic Programs with Assertions and Open PredicatesIsabel Garcia-Contreras, Jose F. Morales and Manuel Hermenegildo
LOPSTR 2019Logic-Based Synthesis of Fair Voting Rules Using Composable ModulesKarsten Diekhoff, Michael Kirsten and Jonas Krämer
LOPSTR 2019Modeling and Reasoning in Event Calculus Using Goal-Directed Constraint Answer Set ProgrammingJoaquin Arias, Zhuo Chen, Manuel Carro and Gopal Gupta
LOPSTR 2019Natural language compositionality in CoqErkki Luuk
LOPSTR 2019On fixpoint/iteration/variant induction principles for proving total correctness of programs with denotational semanticsPatrick Cousot
LOPSTR 2019Semi-Inversion of Conditional Constructor Term Rewriting SystemsMaja Kirkeby and Robert Glück
LOPSTR 2019Solving Proximity ConstraintsTemur Kutsia and Cleo Pau
LOPSTR 2019Synthesizing Imperative Code from Answer Set Programming SpecificationsSarat Chandra Varanasi, Elmer Salazar, Neeraj Mittal and Gopal Gupta
LOPSTR 2019The Prolog debugger and declarative programmingWłodek Drabent
LOPSTR 2019Trace analysis using an Event-driven Interval Temporal LogicMaría-Del-Mar Gallardo and Laura Panizo
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 (MPC Keynote)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 Computations in Mathematical Proofs (MPC Keynote)Assia Mahboubi
MPC 2019Verified Self-Explaining ComputationJan Stolarek and James Cheney
PPDP 201910 Years of the Higher-Order Model Checking Project (Invited Talk)Naoki Kobayashi
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 2019Functional Reactive Programming, restatedGuerric Chupin and Henrik Nilsson
PPDP 2019Functional programming with lambda-tree syntaxUlysse Gerard, Dale Miller and Gabriel Scherer
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 2019Intrinsically-Typed Mechanized Semantics for Session TypesPeter Thiemann
PPDP 2019Moderately Complex Paxos Made Simple: High-Level Executable Specification of Distributed Consensus AlgorithmsYanhong A. Liu, Saksham Chand and Scott Stoller
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 2019Relational Symbolic ExecutionGian Pietro Farina, Stephen Chong and Marco Gaboardi
PPDP 2019Semantic Foundations for Gradual Typing (Invited Talk)Amal Ahmed
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 2019Spacetime Programming: A Synchronous Language for Composable Search StrategiesPierre Talbot
PPDP 2019The PPDP Most Influential Paper 10-Year Award: Foundations of Session TypesMariangiola Dezani
PPDP 2019TopHat: A formal foundation for task-oriented programmingTim Steenvoorden, Nico Naus and Markus Klinik
PPDP 2019Type-Driven Verification of Extra-Functional PropertiesChristopher Mark Brown, Adam Barwell, Yoann Marquer, Celine Minh and Olivier Zendra
PPDP 2019Under Control: Compositionally Correct Closure Conversion with Mutable StatePhillip Mates, Jamie Perconti and Amal Ahmed
RV 2019A Formally Verified Monitor for Metric First-Order Temporal Logic (Regular paper)Joshua Schneider, David Basin, Srdjan Krstic and Dmitriy Traytel
RV 2019Accelerated Learning of Predictive Runtime Monitors for Rare Failure (Regular paper)Reza Babaee, Vijay Ganesh and Sean Sedwards
RV 2019Algorithms for Monitoring Hyperproperties (Tutorial paper)Christopher Hahn
RV 2019AllenRV: an extensible monitor for multiple complex specifications with high reactivity (Demo paper)Nic Volanschi and Bernard Serpette
RV 2019An Extension of LTL with Rules and its Application to Runtime Verification (Regular paper)Klaus Havelund and Doron Peled
RV 2019Assumption-Based Runtime Verification with Partial Observability and Resets (Regular paper)Alessandro Cimatti, Chun Tian and Stefano Tonetta
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 Enforcement (Regular paper)Ian Cassar, Luca Aceto, Adrian Francalanza and Anna Ingólfsdóttir
RV 2019Decentralized Stream Runtime Verification (Regular paper)Luis Miguel Danielsson and César Sánchez
RV 2019Efficient Detection and Quantification of Timing Leaks with Neural Networks (Regular paper)Saeid Tizpaz-Niari, Pavol Cerny, Sriram Sankaranarayanan and Ashutosh Trivedi
RV 2019Explaining Violations of Properties in Control-Flow Temporal Logic (Regular paper)Joshua Dawes and Giles Reger
RV 2019FastCFI: Real-Time Control Flow Integrity using FPGA without Code Instrumentation (Regular paper)Lang Feng, Jeff Huang, Jiang Hu and Abhijith Reddy
RV 2019Monitorability Over Unreliable Channels (Regular paper)Sean Kauffman, Klaus Havelund and Sebastian Fischmeister
RV 2019Neural Predictive Monitoring (Regular paper)Luca Bortolussi, Francesca Cairoli, Nicola Paoletti, Scott Smolka and Scott Stoller
RV 2019NuRV: a nuXmv Extension for Runtime Verification (RV19-demo)Alessandro Cimatti, Chun Tian and Stefano Tonetta
RV 2019On the Runtime Enforcement of Timed Properties (Tutorial paper)Yliès Falcone
RV 2019Overhead-aware deployment of runtime monitors (Short paper)Teng Zhang, Gregory Eakman, Insup Lee and Oleg Sokolsky
RV 2019Predictive Runtime Monitoring for Linear Stochastic Systems and Applications to Geofence Enforcement for UAVs (Regular paper)Hansol Yoon, Yi Chou, Xin Chen, Eric Frew and Sriram Sankaranarayanan
RV 2019Reactive Control Meets Runtime Verification: A Case Study of Navigation (Short paper)Dogan Ulus and Calin Belta
RV 2019Robustness of Specifications and its applications to Falsification, Parameter Mining, and Runtime Monitoring with S-TaLiRo (Tutorial paper)Georgios Fainekos, Bardh Hoxha and Sriram Sankaranarayanan
RV 2019Runtime Verification For Timed Event Streams With Partial Information (Regular paper)Martin Leucker, César Sánchez, Torben Scheffel, Malte Schmitz and Daniel Thoma
RV 2019Shape Expressions for Specifying and Extracting Signal Features (Regular paper)Dejan Nickovic, Xin Qin, Thomas Ferrère, Cristinel Mateis and Jyotirmoy Deshmukh
RV 2019Stream-based Monitoring of Real-time Properties (Tutorial paper)Hazem Torfah
RV 2019Timescales: A Benchmark Generator for Metric Temporal Logic (Benchmark paper)Dogan Ulus
RV 2019Towards Verified Artificial Intelligence: A Run-Time Verification Perspective (Invited Talk)Sanjit A. Seshia
TAP 2019BTestBox - A tool for testing B translators and coverage of B modelsDiego de Azevedo Oliveira, Valério Gutemberg Medeiros Jr, David Déharbe and Martin A. Musicante
TAP 2019Constraints in Dynamic Symbolic Execution: Bitvectors or Integers?Timotej Kapus, Martin Nowack and Cristian Cadar
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 2019Fast and Complete Automatic Structural Unit Test Generation combining Genetic Algorithms and Formal MethodsEric Lavillonnière, David Mentré and Denis Cousineau
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 2019Property-Based Test Case Generators for FreeEmanuele De Angelis, Fabio Fioravanti, Adrian Palacios, Alberto Pettorossi and Maurizio Proietti
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
TAP 2019Sail through your C Code with MetAcsl: Specifying, Testing and Proving High-Level PropertiesVirgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling and Pascale Le Gall
UTP 2019A Calculus of Space, Time and Causality: its Algebra, Geometry, LogicTony Hoare, Georg Struth and Jim Woodcock
UTP 2019A Testing Perspective on Algebraic, Denotational, and Operational SemanticsBernhard K. Aichernig
UTP 2019Connecting Fixpoints of Computations with Strict ProgressWalter Guttmann
UTP 2019Developing an algebra for rely/guarantee concurrencyIan J. Hayes and Larissa Meinicke
UTP 2019Hybrid Relations in Isabelle/UTPSimon Foster
UTP 2019Probabilistic Semantics for RoboChart: A Weakest Completion ApproachJim Woodcock, Ana Cavalcanti, Simon Foster, Alexandre Mota and Kangfeng Ye
UTP 2019The Inner and Outer Algebras of Unified ConcurrencyAndrew Butterfield
UTP 2019UTP Semantics of a Calculus for Mobile Ad Hoc NetworksXi Wu, Huibiao Zhu and Wanling Xie
UTP 2019Unified Graphical Co-Modelling of Cyber-Physical Systems using AADL and Simulink/StateflowHaolan Zhan, Qianqian Lin, Shuling Wang, Jean-Pierre Talpin, Xiong Xu and Naijun Zhan
UTP 2019Whither specifications as programsDavid Naumann and Minh Ngo
VECoS 20191968 to 2019: Half a Century of Correctness Enhancement (Invited Talk)Ali Mili
VECoS 2019Analysing Security Protocols Using Scenario Based SimulationFarah Al-Shareefi, Alexei Lisitsa and Clare Dixon
VECoS 2019Estimating Latency for Synchronous Dataflow Graphs Using Periodic SchedulesPhilippe Glanon, Selma Azaiez and Chokri Mraidha
VECoS 2019Importance-Based Scheduling to Manage Multiple Core Defections in Real-Time SystemsYves Mouafo Tchinda, Annie Choquet-Geniet and Gaëlle Largeteau-Skapin
VECoS 2019Modeling Concurrent Behaviors as WordsJean-Michel Couvreur, Xavier Ferry and Mouhamadou Sakho
VECoS 2019Non-Standard Zeno-Free Simulation Semantics for Hybrid Dynamical SystemsAyman Aljarbouh and Benoît Caillaud
VECoS 2019Running on Fumes -- Preventing Out-of-Gas Vulnerabilities in Ethereum Smart Contracts using Static Resource AnalysisElvira Albert, Pablo Gordillo, Albert Rubio and Ilya Sergey
VECoS 2019Static Detection of Event-Driven Races in HTML5-Based Mobile AppsTuong Lau
VECoS 2019Verifying Robusteness of Concurrent Systems (Invited Talk)Ahmed Bouajjani
AFFORD 2019Addressing usability in a formal development environmentPaolo Arcaini, Silvia Bonfanti, Angelo Gargantini, Elvinia Riccobene and Patrizia Scandurra
AFFORD 2019Compiling C and C++ Programs for White-Box AnalysisZuzana Baranová and Petr Ročkai
AFFORD 2019Experiences on Streamlining Formal Methods Tools (Invited Talk)Paolo Masci
AFFORD 2019Formal Modelling and Verification as Rigorous Review Technology: An Inspiration from INSPEXRichard Banach, Joseph Razavi, Olivier Debicki and Suzanne Lesecq
AFFORD 2019Model Checking in a Development Workflow: A Study on a Concurrent C++ Hash TablePetr Ročkai
AFFORD 2019SEB-CG: Code Generation Tool with Algorithmic Refinement Support for Event-BSadegh Dalvandi and Michael Butler
AFFORD 2019The Bourgeois Gentleman, Engineering and Formal MethodsThierry Lecomte
DALI 2019A Logical Analysis of the Interplay between Social Influence and Friendship SelectionSonja Smets and Fernando R. Velázquez-Quesada
DALI 2019A dynamic epistemic logic analysis of the equality negation taskEric Goubault, Marijana Lazić, Jérémy Ledent and Sergio Rajsbaum
DALI 2019A dynamic logic for QASM programs (Short paper)Carlos Tavares
DALI 2019A four-valued hybrid logic with non-dual modal operatorsDiana Costa and Manuel A. Martins
DALI 2019A labelled sequent calculus for Dynamic Predicate Logic (Short paper)Elio La Rosa
DALI 2019Behavioural and Abstractor Specifications for Dynamic Logic with Binders and Silent TransitionsRolf Hennicker, Alexander Knapp and Alexandre Madeira
DALI 2019Dynamic Preference Logic as a Logic of Belief ChangeMarlo Souza and Alvaro Moreira
DALI 2019Iterative division in the product-free Distributive Full Non-associative Lambek CalculusIgor Sedlar
DALI 2019Mechanizing Bisimulation Theorems for Relation-Changing Logics in CoqRaul Fervari, Francisco Trucco and Beta Ziliani
DALI 2019On the construction of multi-valued concurrent dynamic logic (Short paper)Leandro Gomes
DALI 2019Persuasive Argumentation and Epistemic AttitudesCarlo Proietti and Antonio Yuste-Ginel
DALI 2019Resource separation in Dynamic Logic of Propositional AssignmentsJoseph Boudou, Andreas Herzig and Nicolas Troquard
DALI 2019Social consolidations: Rational belief in a many-valued logic of evidence and peerhood (Short paper)Yuri David Santos
DALI 2019Stit Semantics for Epistemic Notions Based on Information Disclosure in Interactive SettingsAldo Iván Ramírez Abarca and Jan Broersen
DALI 2019TBA (Invited Talk)Dexter Kozen
DALI 2019The Logic of AGM Learning from Partial ObservationsAlexandru Baltag, Aybüke Özgün and Ana Lucia Vargas Sandoval
DALI 2019The Trace ModalityDominic Steinhöfel and Reiner Hähnle
DataMod 2019Diagrammatic physical robot models in RoboSim (Invited Talk)Ana Cavalcanti
DataMod 2019Verification of Data in Space and Time (Invited Talk)Mieke Massink
FMAS 2019A Model Checking Agent-Based Architecture for Representing the Rules of the Road on Autonomous VehiclesGleifer Alves, Louise Dennis and Michael Fisher
FMAS 2019A Temporal Logic Semantics for Teleo-Reactive ProceduresKeith Clark, Brijesh Dongol and Peter Robinson
FMAS 2019CriSGen: Constraint-based Generation of Critical Scenarios for Autonomous VehiclesAndreas Nonnengart, Matthias Klusch and Christian Müller
FMAS 2019TBA (Invited talk)Claudio Menghi
FMAS 2019TBA (Invited talk)Kristin Rozier
FMAS 2019Towards a Mission Definition, Verification and Validation ToolchainLouis Viard, Laurent Ciarletta and Pierre-Etienne Moreau
FMAS 2019Verification of Fair Controllers for Urban Traffic Manoeuvres at IntersectionsMaike Schwammberger and Christopher Bischopink
FMBC 2019A Distributed Blockchain Model of Selfish MiningDennis Eijkel and Ansgar Fehnker
FMBC 2019Call me Back, I have a Type InvariantAnthony Aiello, Johannes Kanig and Taro Kurita
FMBC 2019Deductive Proof of Industrial Smart Contracts Using Why3Zeinab Nehaï and François Bobot
FMBC 2019Formal specification of a security framework for smart contractsMikhail Mandrykin, Jake O'Shannessy, Jacob Payne and Ilya Shchepetkov
FMBC 2019Mi-Cho-Coq, a framework for certifying Tezos Smart ContractsBruno Bernardo, Raphaël Cauderlier, Zhenlei Hu, Basile Pesin and Julien Tesson
FMBC 2019Smart Contract Interactions in Coq (Short paper)Jakob Botsch Nielsen and Bas Spitters
FMBC 2019Smart Contracts: Application Scenarios for Deductive Program Verification (Short paper)Jonas Schiffl, Bernhard Beckert and Mattias Ulbrich
FMBC 2019Solidity 0.5: when typed does not mean type safe (Lightning talk)Silvia Crafa and Matteo Di Pirro
FMBC 2019Statistical Model Checking of RANDAO's Resilience to Pre-computed Reveal StrategiesMusab A. Alturki and Grigore Roşu
FMBC 2019TBA (Invited talk)Ilya Sergey
FMBC 2019Towards Verifying the Bitcoin-S Library (Lightning talk)Ramon Boss, Kai Brünnler and Anna Doukmak
FMBC 2019Towards a Smart Contract Verification Framework in Coq (Lightning talk)Danil Annenkov and Bas Spitters
FMBC 2019Towards a Verified Model of the Algorand Consensus Protocol in Coq (Short paper)Musab A. Alturki, Jing Chen, Victor Luchangco, Brandon Moore, Karl Palmskog, Lucas Peña and Grigore Roşu
FMBC 2019Towards a formally verified implementation of the MimbleWimble cryptocurrency protocol (Lightning talk)Gustavo Betarte, Naximiliano Cristiá, Carlos Luna, Adrián Silveira and Dante Zanarini
FMBC 2019Verifying Smart Contracts with CubicleSylvain Conchon, Alexandrina Korneva and Fatiha Zaïdi
FMTea 2019Logic, Algebra, and Geometry at the Foundation of Computer Science (Invited tutorial)Tony Hoare, Alexandra Mendes and João Ferreira
FMTea 2019Managing Heterogeneity and Bridging the Gap in Teaching Formal MethodsPamela Fleischmann, Mitja Kulczynski, Dirk Nowotka and Thomas Wilke
FMTea 2019On Teaching Applied Formal Methods in Aerospace EngineeringKristin Rozier
FMTea 2019Principled and pragmatic specification of programming languagesAdrian Johnstone and Elizabeth Scott
FMTea 2019TBA (Invited paper)Carroll Morgan
FMTea 2019TBA (Invited tutorial)Holger Hermanns
FMTea 2019TBA (Invited tutorial)Bas Luttik
FMTea 2019Teaching Concurrency with the Disappearing Formal MethodEmil Sekerinski
FMTea 2019Teaching Deductive Verification in Why3 to Undergraduate StudentsSandrine Blazy
FMTea 2019Teaching Discrete Mathematics to Computer Science StudentsFaron Moller and Liam O'Reilly
FMTea 2019Teaching Formal Methods to Future EngineersCatherine Dubois, Virgile Prevosto and Guillaume Burel
FMTea 2019Teaching Formal Methods: From Software in the Small to Software in the LargeMaría-Del-Mar Gallardo and Laura Panizo
FMTea 2019Teaching Formal Methods: Lessons Learnt from Using Event-BNéstor Cataño
FMTea 2019Teaching Introductory Formal Methods and Discrete Mathematics to Software Engineers: Reflections on a modelling-focussed approachAndrew Simpson
FMTea 2019Teaching deductive verification through Frama-C and SPARKChristophe Garion, Jérôme Hugues, Claire Dross, Joffrey Huguet and Léo Creuse
FMTea 2019The Computational Relevance of Formal Logic through Formal ProofsAriane A. Almeida, Ana Cristina Rocha-Oliveira, Thiago Mendonça Ferreira Ramos, Flavio L. C. De Moura and Mauricio Ayala-Rincon
FMTea 2019Using Krakatoa for teaching formal verification of Java programsJose Divasón and Ana Romero
FMTea 2019You already used Formal Methods but did not knowGiampaolo Bella
HFM 2019Babbage's mechanical notationAdrian Johnstone and Elizabeth Scott
HFM 2019Formal specifications and software testing: a fruitful convergenceMarie-Claude Gaudel
HFM 2019From manuscripts to programming languages: an archivist perspectiveAlexandra Vidal, Ana Sandra Meneses and António Sousa
HFM 2019History of Abstract InterpretationFrancesco Ranzato and Roberto Giacobazzi
HFM 2019Reasoning about shared-variable concurrency: interactions between research threadsCliff Jones
HFM 2019Specification with class: A brief history of Object-ZDavid Duke and Graeme Smith
HFM 2019The History and Evolution of B and Event-BSebastian Krings, Michael Butler, Philipp Koerner, Thierry Lecomte, Michael Leuschel and Laurent Voison
HFM 2019The Prehistory and History of Requirements Engineering (RE) (+ Software Engineering) as Seen by Me: How my interest in Formal Methods eventually moved me to REDaniel Berry
HFM 2019The School of Squiggol: A History of the Bird-Meertens FormalismJeremy Gibbons
HFM 2019The early history of flow diagrams as a formal method (Invited Talk)Mark Priestley
REFINE 2019A Map of Asynchronous Communication ModelsFlorent Chevrou, Aurélie Hurault and Philippe Queinnec
REFINE 2019An abstract semantics of speculative execution for reasoning about security vulnerabilitiesRobert Colvin and Kirsten Winter
REFINE 2019Comparing Correctness-by-Construction with Post-hoc Verification - A Qualitative User StudyTobias Runge, Thomas Thüm, Loek Cleophas, Ina Schaefer and Bruce Watson
REFINE 2019Exploring the use of Rely/Guarantee Reasoning for Non-blocking Algorithms (Short paper)Nisansala Yatapanage
REFINE 2019TBA (Invited talk)Régine Laleau
REFINE 2019Towards a Method for the Decomposition by Refinement in Event-B (Short paper)Kenza Kraibi, Rahma Ben Ayed, Joris Rehm, Simon Collart-Dutilleul, Philippe Bon and Dorian Petit
REFINE 2019Transformations for Generating Type RefinementsDouglas Smith and Stephen Westfold
REFINE 2019Weakening correctness and linearizability for concurrent objects on multicore processorsGraeme Smith and Lindsay Groves
SASB 2019Bayesian Verification of Chemical Reaction NetworksGareth Molyneux, Viraj Brian Wijesuriya and Alessandro Abate
SASB 2019Biochemical pathways from causal cores in rule-based modellingSébastien Légaré
SASB 2019Kappa Site-graph Patterns Equations ResolutionYvan Sraka and Jérôme Feret
SASB 2019Nested Event Representation for Automated Assembly of Cell Signaling Network ModelsEvan Becker, Kara Bocan and Natasa Miskov-Zivanov
SASB 2019Specification and Analysis of Biochemical Systems in BCSLMatej Troják, David Šafránek, Jan Červený, Luboš Brim and Lukrécia Mertová
SASB 2019TBA (Keynote talk)Miguel Rocha
SASB 2019TBA (Keynote talk)Anne Siegel