Programme
Programme of main conferences from Monday to Thursday. Distinguished papers are highlighted in yellow and by asterisk.
Thursday 08 May
09:00
10:00
Coffee Break
TACAS: Games
Room:
10:30
Reachability for Nonsmooth Systems with Lexicographic Jacobians
Chenxi Ji, Huan Zhang and Sayan Mitra
11:00
Non-Zero-Sum Games with Multiple Weighted Objectives*
Yoav Feisntein, Orna Kupferman and Noam Shenwald
11:30
Fast value iteration: A uniform approach to efficient algorithms for energy games
Michaël Cadilhac, Antonio Casares and Pierre Ohlmann
12:00
Proxy Attribute Discovery in Machine Learning Datasets via Inductive Logic Programming
Rafael Gonçalves, Filipe Gouveia, Inês Lynce and José Fragoso Santos
ESOP: Probabilistic Programming
Room:
10:30
Verifying Algorithmic Versions of the Lovász Local Lemma
Rongen Lin, Hongjin Liang and Xinyu Feng
11:00
A Program Logic for Concurrent Randomized Programs in the Oblivious Adversary Model
Weijie Fan, Hongjin Liang, Xinyu Feng and Hanru Jiang
11:30
Variable Elimination as Rewriting in a Linear Lambda Calculus
Claudia Faggian, Thomas Ehrhard and Michele Pagani
12:00
A Complete Axiomatisation of Equivalence for Discrete Probabilistic Programming
Robin Piedeleu, Mateo Torres-Ruiz, Alexandra Silva and Fabio Zanasi
SPIN: None
Room:
10:30
12:30
Lunch
TACAS: Verification II
Room:
14:00
Dynamic Verification of OCaml Software with Gospel and Ortac/QCheck-STM*
Nikolaus Huber, Naomi Spargo, Nicolas Osborne, Samuel Hym and Jan Midtgaard
14:30
Pushing the Limit: Verified Performance-Optimal Causally-Consistent Database Transactions
Shabnam Ghasemirad, Christoph Sprenger, Si Liu, Luca Multazzu and David Basin
15:00
Weakly acyclic diagrams: A data structure for infinite-state symbolic verification
Michael Blondin, Michaël Cadilhac, Xin-Yi Cui, Philipp Czerner, Javier Esparza and Jakob Schulz
15:30
Certifiably Robust Policies for Uncertain Parametric Environments
Yannik Schnitzer, Alessandro Abate and David Parker
ESOP: Verification
Room:
14:00
Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration
Florian Sextl, Adam Rogalewicz, Tomáš Vojnar and Florian Zuleger.
14:30
CUTECat: Concolic Execution for Computational Law
Pierre Goutagny, Aymeric Fromherz and Raphaël Monat
15:00
Coma, an Intermediate Verification Language with Explicit Abstraction Barriers
Andrei Paskevich, Paul Patault and Jean-Christophe Filliâtre
15:30
Cognacy Queries over Dependence Graphs for Transparent Visualisations
Joseph Bond, Cristina David, Minh Nguyen, Dominic Orchard and Roly Perera
SPIN: None
Room:
14:00
Award session
Chair:
Room:
14:00
TestComp
Chair:
Room:
14:00
16:00
Coffee Break
TACAS: Quantum & GPU
Room:
16:30
GPUexplore-prob: Markov Chain State Space Construction and Verification with GPUs
Jan Heemstra and Anton Wijs
16:45
SliQSim: A Quantum Circuit Simulator and Property Checker
Tian-Fu Chen and Jie-Hong Roland Jiang
17:00
AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs
Yu-Fang Chen, Kai-Min Chung, Min-Hsiu Hsieh, Wei-Jia Huang, Ondrej Lengal, Jyun-Ao Lin and Wei-Lun Tsai
17:30
Parallel Equivalence Checking of Stabilizer Quantum Circuits on GPUs
Muhammad Osama, Dimitrios Thanos and Alfons Laarman
ESOP: Concurrency 2
Room:
16:30
Sufficient Conditions for Robustness of RDMA Programs
Guillaume Ambal, Ori Lahav and Azalea Raad
17:00
Formulas as Processes, Deadlock-freedom as Choreographies
Matteo Acclavio, Giulia Manara and Fabrizio Montesi
17:30
Constructive characterisations of the must-preorder for asynchrony
Giovanni Bernardi, Ilaria Castellani, Paul Laforgue and Léo Stefanesco
SPIN: None
Room:
16:30
TestComp
Chair:
Room:
16:30