ETAPS 2020

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

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

Invited Tutorial

Combining machine learning and formal methods

Madhusudan Parthasarathy

Room: Carlisle Suite

16:30 – 18:00

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

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

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

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

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

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

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

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

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