Detailed program of iFM 2020

Proceedings of iFM 2020

Videos of the invited talks and paper presentations.

Invited Speakers

Edward A. Lee (University of California at Berkeley, United States)

David Parker (University of Birmingham, United Kingdom)

Hongseok Yang (School of Computing, KAIST, Korea)

Accepted Papers

PALM: a technique for Process ALgebraic specification Mining
Sara Belluccini, Rocco De Nicola, Barbara Re and Francesco Tiezzi

Modular Integration of Crashsafe Caching into a Verified Virtual File System Switch
Stefan Bodenmüller, Gerhard Schellhorn and Wolfgang Reif

Formal Verification of Executable Complementation and Equivalence Checking for Büchi Automata
Julian Brunner

Lock and Fence When Needed: State Space Exploration + Static Analysis = Improved Fence and Lock Insertion
Sander de Putter and Anton Wijs

Chain of events: Modular Process Models for the Law
Søren Debois, Hugo A. López, Tijs Slaats, Amine Abbad Andaloussi and Thomas Hildebrandt

An Event-B Based Generic Framework for Hybrid Systems Formal Modelling
Guillaume Dupont, Yamine Ait Ameur, Marc Pantel and Neeraj Singh

Grey-Box Learning of Register Automata
Bharat Garhewal, Frits Vaandrager, Falk Howar, Timo Schrijvers, Toon Lenaerts and Rob Smits

Active Objects with Deterministic Behaviour
Ludovic Henrio, Einar Broch Johnsen and Violet Ka I Pun

History-based Specification and Verification of Java Collections in KeY
Hans-Dieter Hiep, Jinting Bian, Frank De Boer and Stijn De Gouw

Algebra-based Loop Synthesis
Andreas Humenberger, Nikolaj Bjorner and Laura Kovacs

Meeduse: A Tool to Build and Run Proved DSLs
Akram Idani

Reformulation of SAT into a Polynomial Box-Constrained Optimization Problem (Short Paper)
Stéphane Jacquet and Sylvain Hallé

Formal Policy Synthesis for Continuous-State Systems via Reinforcement Learning
Milad Kazemi and Sadegh Soudjani

Fast and Effective Well-Definedness Checking for Formal Models
Michael Leuschel

Detection of Polluting Test Objectives for Dataflow Criteria
Thibault Martin, Nikolai Kosmatov, Virgile Prevosto and Matthieu Lemerre

Clustering-Guided SMT(LRA) Learning
Tim Meywerk, Marcel Walter, Daniel Große and Rolf Drechsler

Jaint: A Framework for User-Defined Dynamic Taint-Analyses based on Dynamic Symbolic Execution of Java Programs
Malte Mues, Till Schallau and Falk Howar

Synthesizing clock-efficient timed automata
Neda Saeedloei and Feliks Kluzniak

A Generic Approach to the Verification of the Permutation Property of Sequential and Parallel Swap-based Sorting Algorithms
Mohsen Safari and Marieke Huisman

Tight Error Analysis in Fixed-point Arithmetic
Stella Simic, Alberto Bemporad, Omar Inverso and Mirco Tribastone

Generating SPARK from Event-B Models
Sanjeevan Sritharan and Thai Son Hoang

Philosophers may Dine - Definitively!
Safouan Taha, Lina Ye and Burkhart Wolff

Automatic Generation of Guard-Stable Floating-Point Code
Laura Titolo, Mariano Moscato, Marco Antonio Feliu Gabaldon and Cesar Munoz

Formal methods for GPGPU programming: is the demand met?
Lars B. van den Haak, Anton Wijs, Mark van den Brand and Marieke Huisman