ETAPS 2020

Detailed Program

Monday

27 April 2020

Tuesday

28 April 2020

Wednesday

29 April 2020

Thursday

30 April 2020

Monday

27 April 2020

Registration

08:00

Invited Talk

Jane Hillston

Title: TBA

Room: Carlisle Suite

09:00-10:00

Coffee Break

10:00-10:30

TACAS

Program Verification

Room: Carlisle Suite

10:30-11:00
Software Verification with PDR: An Implementation of the State of the Art

Dirk Beyer and Matthias Dangl

11:00-11:30
Verifying Array Manipulating Programs with Full-Program Induction

Supratik Chakraborty, Ashutosh Gupta and Divyesh Unadkat

11:30-12:00
Interpretation-Based Violation Witness Validation for C: NITWIT

Jan Svejda, Philipp Berger and Joost-Pieter Katoen

12:00-12:30
A Calculus for Modular Loop Acceleration

Florian Frohn
Nominations: EAPLS Award for the best ETAPS paper on PL and systems, EASST Award-systematic and rigorous engineering of SW & systems

FoSSaCS

Room: Martello 1 Suite

10:30-11:00
Deep induction: Induction rules for (truly) nested types
Patricia Johann and Andrew Polonsky

11:00-11:30
A Curry-style semantics of interaction
James Laird

11:30-12:00
Quantum programming with inductive datatypes: causality and affine type theory
Romain Péchoux, Simon Perdrix, Mathys Rennela and Vladimir Zamdzhiev

12:00-12:30
Non-idempotent intersection types in logical form
Thomas Ehrhard

Lunch Break

12:30-14:00

TACAS

SAT & SMT

Room: Carlisle Suite

14:00-14:30
Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic
Takamasa Okudono and Andy King

14:30-15:00
Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers
Daniele Ahmed, Andrea Peruffo and Alessandro Abate

15:00-15:30
A Study of Symmetry Breaking Predicates and Model Counting
Wenxi Wang, Muhammad Usman, Alyas Almaawi, Kaiyuan Wang, Kuldeep S. Meel and Sarfraz Khurshid

15:30-16:00
MUST: Minimal Unsatisfiable Subsets Enumeration Tool
Jaroslav Bendík and Ivana Cerna

ESOP

Concurrency and distribution

Room: Kingstown Suite

14:00-14:30
Modular Relaxed Dependencies in Weak Memory Concurrency
Marco Paviotti, Simon Cooksey, Anouk Paradis, Daniel Wright, Scott Owens and Mark Batty

14:30-15:00
Verifying Visibility-Based Weak Consistency
Siddharth Krishna, Michael Emmi, Constantin Enea and Dejan Jovanović

15:00-15:30
Proving the safety of highly-available distributed objects
Sreeja S Nair, Gustavo Petri and Marc Shapiro
Nomination: EASST Award-systematic and rigorous engineering of SW & systems

15:30-16:00
ARMv8-A system semantics: instruction fetch in relaxed architectures
Ben Simner, Shaked Flur, Christopher Pulte, Alasdair Armstrong, Jean Pichon-Pharabod, Luc Maranget and Peter Sewell
Nomination: EAPLS Award for the best ETAPS paper on PL and systems

FoSSaCS

Room: Martello 1 Suite

14:00-14:30
Minimal coverability tree construction made complete and efficient
Alain Finkel, Serge Haddad and Igor Khmelnitsky

14:30-15:00
The inconsistent labelling problem of stutter-preserving partial-order reduction
Thomas Neele, Antti Valmari and Tim Willemse
Nominations: EATCS Award for the best ETAPS paper in theoretical computer science, EASST Award for the best ETAPS paper related to the systematic and rigorous engineering of software and systems.

15:00-15:30
The polynomial complexity of vector addition systems with states
Florian Zuleger

15:30-16:00
Ambiguity, weakness, and regularity in probabilistic Büchi automata
Anton Pirogov and Christof Löding

Coffee Break

16:00-16:30

Invited Tutorial

Combining machine learning and formal methods

Madhusudan Parthasarathy
Room: Carlisle Suite

16:30 – 18:00

TACAS

Timed & Dynamical Systems

Room: Kingstown Suite

16:30-17:00
Safe Decomposition of Startup Requirements: Verification and Synthesis
Alessandro Cimatti, Luca Geatti, Alberto Griggio, Greg Kimberly and Stefano Tonetta

17:00-17:30
Multi-Agent Safety Verification using Symmetry Transformations
Hussein Sibai, Navid Mokhlesi, Chuchu Fan and Sayan Mitra

17:30-18:00
Relational Differential Dynamic Logic
Juraj Kolčák, Jérémy Dubut, Ichiro Hasuo, Shin-Ya Katsumata, David Sprunger and Akihisa Yamada

Welcome Reception

19:00 – 20:30

Tuesday

28 April 2020

Registration

08:30

Invited Talk

Scott Smolka

Neural Flight Formation

Room: Carlisle Suite

09:00-10:00

Coffee Break

10:00-10:30

TACAS

Verifying Concurrent Systems

Room: Carlisle Suite

10:30-11:00
Assume, Guarantee or Repair
Hadar Frenkel, Orna Grumberg, Corina Pasareanu and Sarai Sheinvald

11:00-11:30
Structural Invariants for the Verification of Systems with Parameterized Architectures
Marius Bozga, Javier Esparza, Radu Iosif, Joseph Sifakis and Christoph Welzel

11:30-12:00
Automated Verification of Parallel Nested DFS
Wytse Oortwijn, Marieke Huisman, Sebastiaan Joosten and Jaco van de Pol

12:00-12:30
Discourje: Runtime Verification of Communication Protocols in Clojure
Ruben Hamers and Sung-Shik Jongmans

ESOP

Language design and implementation

Room: Kingstown Suite

10:30-11:00
Trace-Relating Compiler Correctness and Secure Compilation
Carmine Abate, Roberto Blanco, Stefan Ciobaca, Deepak Garg, Catalin Hritcu, Marco Patrignani, Éric Tanter and Jérémy Thibault
Nomination: EATCS Award for the best ETAPS paper in theoretical computer science

11:00-11:30
Runners in action
Danel Ahman and Andrej Bauer

11:30-12:00
Compositional Control-Flow Analysis
Kimball Germane and Michael Adams

12:00-12:30
Higher-Order Spreadsheets with Spilled Arrays
Jack Williams, Nima Joharizadeh, Andrew Gordon and Advait Sarkar

FoSSaCS

Room: Martello 1 Suite

10:30-11:00
Concurrent Kleene algebra with observations: From hypotheses to completeness
Tobias Kappé, Paul Brunet, Alexandra Silva, Jana Wagemaker and Fabio Zanasi

11:00-11:30
Contextual equivalence for signal flow graphs
Filippo Bonchi, Robin Piedeleu, Pawel Sobocinski and Fabio Zanasi

11:30-12:00
Learning weighted automata over principal ideal domains
Gerco van Heerdt, Clemens Kupke, Jurriaan Rot and Alexandra Silva

12:00-12:30
Supervised learning as change propagation with delta lenses
Zinovy Diskin

Lunch Break

12:30-14:00

TACAS

Probabilistic Systems

Room: Carlisle Suite

14:00-14:30
Scenario-Based Verification of Uncertain MDPs
Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen and Ufuk Topcu

14:30-15:00
Good-for-MDPs Automata for Probabilistic Analysis and Reinforcement Learning
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi and Dominik Wojtczak

15:00-15:30
Farkas certificates and minimal witnesses for probabilistic reachability constraints
Florian Funke, Simon Jantsch and Christel Baier

15:30-16:00
Simple Strategies in Multi-Objective MDPs
Florent Delgrange, Joost-Pieter Katoen, Tim Quatmann and Mickael Randour

ESOP

Type systems

Room: Kingstown Suite

14:00-14:30
Higher-Ranked Annotation Polymorphic Dependency Analysis
Fabian Thorand and Jurriaan Hage

14:30-15:00
Exploring Type-Level Bisimilarity towards More Expressive Multiparty Session Types
Sung-Shik Jongmans and Nobuko Yoshida

15:00-15:30
A Modular Inference of Linear Types for Multiplicity-Annotated Arrows
Kazutaka Matsuda

15:30-16:00
Mixed Sessions
Vasco Vasconcelos, Filipe Casal, Bernardo Almeida and Andreia Mordido

FoSSaCS

Room: Martello 1 Suite

14:00-14:30
Timed negotiations
S. Akshay, Blaise Genest, Loic Helouet and Sharvik Mital

14:30-15:00
An axiomatic approach to reversible computation
Ivan Lanese, Iain Phillips and Irek Ulidowski

15:00-15:30
On the k-synchronizability of systems
Cinzia Di Giusto, Laetitia Laversa and Etienne Lozes

15:30-16:00
Controlling a random population
Thomas Colcombet, Nathanaël Fijalkow and Pierre Ohlmann

FASE

Security, Distribution & Streams

Room: Martello 2 Suite

14:00-14:30
A General Formal Semantic Framework for Smart Contracts
Jiao Jiao, Shang-Wei Lin and Jun Sun

14:30-15:00
Algorithmic Analysis of Blockchain Efficiency with Communication Delay
Carlos Pinzón, Camilo Rocha and Jorge Finke

15:00-15:30
Global Reproducibility through Local Control for Distributed Active Objects
Lars Tveito, Einar Broch Johnsen and Rudolf Schlatte

15:30-16:00
An Empirical Study on the Use and Misuse of Java 8 Streams
Raffi Khatchadourian, Yiming Tang, Mehdi Bagherzadeh and Baishakhi Ray
Nominations: EAPLS Award for the best ETAPS paper on PL and systems, EASST Award-systematic and rigorous engineering of SW & systems

Test-Comp

2nd Intl. Competition on Software Testing

Room: Mariner Suite

14:00-16:00

Test-Comp 2020

Presentations

Coffee Break

16:00-16:30

Invited Tutorial

Reachability Analysis Techniques for Hybrid Systems

Erika Ábrahám
Room: Carlisle Suite

16:30 – 18:00

TACAS

Model Checking and Reachability

Room: Kingstown Suite

16:30-18:00

Partial Order Reduction for Deep Bug Finding in Synchronous Hardware
Makai Mann and Clark Barrett

Revisiting Underapproximate Reachability for Multipushdown Systems
S. Akshay, Paul Gastin, Krishna S and Sparsa Roychoudhary

KReach: A Tool for Reachability in Petri Nets
Alex Dixon and Ranko Lazic

AVR: Abstractly Verifying Reachability
Aman Goel and Karem Sakallah

Test-Comp

2nd Intl. Competition on Software Testing

Room: Mariner Suite

16:30-18:00

Test-Comp 2020

Community Meeting

Wednesday

29 April 2020

Registration

08:30

Invited Talk

Işıl Dillig

Formal Methods for Evolving Database Applications

Room: Carlisle Suite

09:00-10:00

Coffee Break

10:00-10:30

TACAS

Timed & Probabilistic System

Room: Carlisle Suite

10:30-11:00
Towards Practical Verification of Reachability Checking for Timed Automata
Simon Wimmer and Joshua von Mutius

11:00-11:30
Learning One-Clock Timed Automata
Jie An, Mingshuai Chen, Bohua Zhan, Naijun Zhan and Miaomiao Zhang

11:30-12:00
Rare event simulation for non-Markovian repairable fault trees
Carlos E. Budde, Marco Biagi, Raúl E. Monti, Pedro R. D’Argenio and Mariëlle Stoelinga

12:00-12:15
FIG: the Finite Improbability Generator
Carlos E. Budde

12:15-12:30
MORA – Automatic Generation of Moment-Based Invariants

Miroslav Stankovic, Ezio Bartocci and Laura Kovacs

ESOP

Program analysis and synthesis

Room: Kingstown Suite

10:30-11:00
Concise Read-Only Specifications for Better Synthesis of Programs with Pointers
Andreea Costea, Amy Zhu, Nadia Polikarpova and Ilya Sergey

11:00-11:30
Optimal and Perfectly Parallel Algorithms for On-demand Data-flow Analysis
Krishnendu Chatterjee, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen and Andreas Pavlogiannis
Nomination: EATCS Award for the best ETAPS paper in theoretical computer science

11:30-12:00
Solving Program Sketches with Large Integer Values
Rong Pan, Qinheping Hu, Rishabh Singh and Loris D’Antoni
Nomination: EAPLS Award for the best ETAPS paper on PL and systems

12:00-12:30
Continualization of Probabilistic Programs With Correction
Jacob Laurel and Sasa Misailovic

FoSSaCS

Room: Martello 1 Suite

10:30-11:00
Spinal atomic lambda-calculus
David Sherratt, Willem Heijltjes, Michel Parigot and Tom Gundersen

11:00-11:30
Decomposing probabilistic lambda-calculi
Ugo Dal Lago, Giulio Guerrieri and Willem Heijltjes

11:30-12:00
Constructing infinitary quotient-inductive types
Marcelo Fiore, Andrew Pitts and Shaun Steenkamp

12:00-12:30
Semantical analysis of contextual types
Brigitte Pientka and Ulrich Schöpp

FASE

Variability & Patterns

Room: Martello 2 Suite

10:30-11:00
Multi-level Model Product Lines: Open and closed variability for modelling language families
Juan De Lara and Esther Guerra

11:00-11:30
Family-Based SPL Model Checking Using Parity Games with Variability
Maurice H. ter Beek, Sjef van Loo, Erik de Vink and Tim Willemse

11:30-12:00
Statistical Model Checking for Variability-Intensive Systems
Maxime Cordy, Mike Papadakis and Axel Legay

12:00-12:30
Analysis and Refactoring of Software Systems Using Performance Antipattern Profiles
Radu Calinescu, Vittorio Cortellessa, Ioannis Stefanakos and Catia Trubiani

Lunch Break

12:30-14:00

TACAS

Bisimulation

Room: Carlisle Suite

14:00-14:30
An O(m log n) algorithm for branching bisimilarity on labelled transition systems
David N. Jansen, Jan Friso Groote, Jeroen J. A. Keiren and Anton Wijs

14:30-15:00
Verifying Quantum Communication Protocols with Ground Bisimulation
Xudong Qin and Yuxin Deng

15:00-15:30
Deciding the bisimilarity of context-free session types
Bernardo Almeida, Andreia Mordido and Vasco T. Vasconcelos

15:30-16:00
Congruences Adequate with Temporal Logics Combining Weak and Strong Modalities
Frédéric Lang, Radu Mateescu and Franco Mazzanti

ESOP

Verification and ownership

Room: Kingstown Suite

14:00-14:30
ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs
John Toman, Ren Siqi, Kohei Suenaga, Atsushi Igarashi and Naoki Kobayashi

14:30-15:00
Local Reasoning for Global Graph Properties
Siddharth Krishna, Alexander J. Summers and Thomas Wies

15:00-15:30
Connecting Higher-Order Separation Logic to a First-Order Outside World
William Mansky, Wolf Honore and Andrew Appel

15:30-16:00
RustHorn: CHC-based Verification for Rust Programs
Yusuke Matsushita, Takeshi Tsukada and Naoki Kobayashi

FoSSaCS

Room: Martello 1 Suite

14:00-14:30
Graded algebraic theories
Satoshi Kura

14:30-15:00
On well-founded and recursive coalgebras
Jiri Adamek, Stefan Milius and Larry Moss

15:00-15:30
A duality theoretic view on limits of finite structures
Mai Gehrke, Tomáš Jakl and Luca Reggio

15:30-16:00
Local local reasoning: A BI-hyperdoctrine for full ground store
Miriam Polzer and Sergey Goncharov

FASE

Analysis

Room: Martello 2 Suite

14:00-14:30
Platinum: Reusing Constraint Solutions in Bounded Analysis of Relational Logic
Guolong Zheng, Hamid Bagheri, Gregg Rothermel and Jianghao Wang

14:30-15:00
Skill-Based Verification of Cyber-Physical Systems
Alexander Knüppel, Inga Jatzkowski, Marcus Nolte, Thomas Thüm, Tobias Runge and Ina Schaefer

15:00-15:30
Revisiting semantics of interactions for trace validity analysis
Erwan Mahe, Christophe Gaston and Pascale Le Gall

15:30-16:00
Extracting Semantics from Question-Answering Services for Snippet Reuse
Themistoklis Diamantopoulos, Nikolaos Oikonomou and Andreas Symeonidis

Coffee Break

16:00-16:30

TACAS

Verification & efficiency

Room: Carlisle Suite

16:30-17:00
How Many Bits Does it Take to Quantize Your Neural Network?
Mirco Giacobbe, Thomas Henzinger and Mathias Lechner

17:00-17:30
Highly Automated Formal Proofs over Memory Usage of Assembly Code

Freek Verbeek, Joshua Bockenek and Binoy Ravindran
Nomination: EASST Award-systematic and rigorous engineering of SW & systems

17:30-17:45
GASOL: Gas Analysis and Optimization for Ethereum Smart Contracts

Elvira Albert, Jesús Correas, Pablo Gordillo, Guillermo Román-Díez and Albert Rubio

17:45-18:00
CPU Energy Meter: A Tool for Energy-Aware Algorithms Engineering
Dirk Beyer and Philipp Wendler

ESOP

Semantics

Room: Kingstown Suite

16:30-17:00
Soundness conditions for big-step semantics

Francesco Dagnino, Viviana Bono, Elena Zucca and Mariangiola Dezani-Ciancaglini

17:00-17:30
SMT-Friendly Formalization of the Solidity Memory Model

Ákos Hajdu and Dejan Jovanović

17:30-18:00
Semantic Foundations for Deterministic Dataflow and Stream Processing
Konstantinos Mamouras

FASE

Model-based Design

Room: Martello 2 Suite

16:30-17:00
Generating Large EMF Models Efficiently: A Rule-Based, Configurable Approach
Nebras Nassar, Jens Kosiol, Timo Kehrer and Gabriele Taentzer

17:00-17:30
Model-based tool support for Service Design

Francisco Javier Perez Blanco, Juan Manuel Vara, Cristian Gómez Macías, María Valeria De Castro and Esperanza Marcos

17:30-18:00
Business Process Compliance using Reference Models of Law
Hugo A. López, Søren Debois, Tijs Slaats and Thomas Hildebrandt

Tour & Conference Dinner

18:30 – 22:30

Thursday

30 April 2020

Registration

08:30

Invited Talk

Willem Visser

The Magic of Analyzing Programs

Room: Carlisle Suite

09:00-10:00

Coffee Break

10:00-10:30

TACAS

Logic and Proof

Room: Carlisle Suite

10:30-11:00
Practical Machine-Checked Formalization of Change Impact Analysis
Karl Palmskog, Ahmet Celik and Milos Gligoric

11:00-11:30
What’s Decidable About Program Verification Modulo Axioms?

Umang Mathur, P. Madhusudan and Mahesh Viswanathan

11:30-12:00
Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting

Alexander Lochmann and Aart Middeldorp

12:00-12:30
Fold/Unfold Transformations for Fixpoint Logic
Naoki Kobayashi, Grigory Fedyukovich and Aarti Gupta

ESOP

Logic and foundations

Room: Kingstown Suite

10:30-11:00
A First-Order Logic with Frames

Christof Löding, P. Madhusudan, Adithya Murali and Lucas Peña
Nomination: EASST Award-systematic and rigorous engineering of SW & systems

11:00-11:30
Constructive Game Logic
Brandon Bohrer and André Platzer

11:30-12:00
On the Versatility of Open Logical Relations: Continuity, Automatic Differentiation, and a Containment Theorem
Gilles Barthe, Raphaëlle Crubillé, Ugo Dal Lago and Francesco Gavazzo

12:00-12:30
Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems

Morten Krogh-Jespersen, Amin Timany, Marit Edna Ohlenbusch, Simon Gregersen and Lars Birkedal

FoSSaCS

Room: Martello 1 Suite

10:30-11:00
On computability of data word functions defined by transducers
Léo Exibard, Emmanuel Filiot and Pierre-Alain Reynier

11:00-11:30
Parameterized synthesis for fragments of first-order logic over data words
Béatrice Bérard, Benedikt Bollig, Mathieu Lehaut and Nathalie Sznajder

11:30-12:00
An auxiliary logic on trees: on the Tower-hardness of logics featuring reachability and submodel reasoning
Alessio Mansutti

12:00-12:30
Exponential automatic amortized resource
David Kahn and Jan Hoffmann

FASE

Model Checking & Specification

Room: Martello 2 Suite

10:30-11:00
Integrating model checking and topological proofs to instrument iterative design
Claudio Menghi, Alessandro Maria Rizzi and Anna Bernasconi

11:00-11:30
Computing Program Reliability using Forward-Backward Precondition Analysis and Model Counting
Aleksandar S. Dimovski and Axel Legay

11:30-12:00
Combining Partial Specifications using Alternating Interface Automata
Ramon Janssen

12:00-12:30
Holistic Specifications for Robust Programs
Susan Eisenbach, Sophia Drossopoulou, James Noble and Julian Mackay

Lunch Break

12:30-14:00

TACAS

Tools & case studies

Room: Carlisle Suite

14:00-14:30
Verifying OpenJDK’s LinkedList using KeY
Hans-Dieter Hiep, Olaf Maathuis, Jinting Bian, Frank De Boer, Marko Van Eekelen and Stijn De Gouw

14:30-15:00
Analysing installation scenarios of Debian packages

Benedikt Becker, Nicolas Jeannerod, Claude Marché, Yann Régis-Gianas, Mihaela Sighireanu and Ralf Treinen

15:00-15:30
Endicheck: Dynamic Analysis for Detecting Endianness Bugs

Roman Kapl and Pavel Parizek

15:30-15:45
Describing and Simulating Concurrent Quantum Systems
Richard Bornat, Jaap Boender, Florian Kammueller, Guillaume Poly and Rajagopal Nagarajan

15:45-16:00
EMTST: Engineering the Meta-theory of Session Types

David Castro-Perez, Francisco Ferreira and Nobuko Yoshida

FoSSaCS

Room: Martello 1 Suite

14:00-14:30
Cartesian difference categories

Mario Alvarez-Picallo and Jean-Simon Lemay

14:30-15:00
Correctness of automatic differentiation via diffeologies and categorical gluing

Mathieu Huot, Sam Staton and Matthijs Vákár
Nomination: EATCS Award for the best ETAPS paper in theoretical computer science, EAPLS Award for the best ETAPS paper on programming languages and systems.

15:00-15:30
Relative full completeness for bicategorical cartesian closed structure

Marcelo Fiore and Philip Saville

FASE

Model Consistency & Synchronization

Room: Martello 2 Suite

14:00-14:30
Automated Generation of Consistent Graph Models with First-Order Logic Theorem Provers
Aren Babikian, Oszkár Semeráth and Daniel Varro

14:30-15:00
Towards Multiple Model Synchronization with Comprehensive Systems

Patrick Stünkel, Harald König, Yngve Lamo and Adrian Rutle

15:00-15:30
Incremental Concurrent Model Synchronization using Triple Graph Grammars

Fernando Orejas, Elvira Pino and Marisa Navarro

15:30-16:00
Schema Compliant Consistency Management via Triple Graph Grammars and Integer Linear Programming
Nils Weidmann and Anthony Anjorin

SVComp

9th Intl. Competition on Software Verification

Room: Kingstown Suite

14:00-16:00

Session 1

Coffee Break

16:00-16:30

TACAS

Games & Automata

Room: Carlisle Suite

16:30-17:00
Solving Mean-Payoff Games via Quasi Dominions
Massimo Benerecetti, Daniele Dell’Erba and Fabio Mogavero
Nomination: EATCS Award for the best ETAPS paper in theoretical computer science

17:00-17:30
Partial-Order Reduction for Parity Games with an Application on Parameterised Boolean Equation Systems

Thomas Neele, Tim Willemse and Wieger Wesselink

17:30-18:00
Polynomial Identification of $\omega$-Automata

Dana Angluin, Dana Fisman and Yaara Shoval

SVComp

9th Intl. Competition on Software Verification

Room: Kingstown Suite

16:30-18:00

Session 2