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