Programme
Programme of main conferences from Monday to Thursday. Best Paper candidates are highlighted in yellow and by asterisk.
Wednesday 26 April
9:00
Véronique Cortier: Electronic Voting: Design And Formal Verification (unifying talk)
Chair: Orna Kupferman
Room: Auditorium
10:00
Coffee break
Room: Foyer + 44 lobby
TACAS: Combinatorial Optimization / Theorem Proving
Chair: Haniel Barbosa
Room: Auditorium
10:30
New Core-Guided and Hitting Set Algorithms for Multi-Objective Combinatorial Optimization
J. Cortes, I. Lynce, V. Manquinho
11:00
Verified reductions for optimization
A. Bentkamp, R. Fernández Mir, J. Avigad
11:30
Specifying and Verifying Higher-order Rust Iterators
X. Denis, J. Jourdan
12:00
Extending a High-Performance Prover to Higher-Order Logic
P. Vukmirović, J. Blanchette, S. Schulz
TACAS: Tools (Regular Papers)
Chair: Alessandro Cimatti
Room: 44-45/108
10:30
The WhyRel Prototype for Relational Verification of Pointer Programs*
R. Nagasamudram, A. Banerjee, D. Naumann
11:00
Bridging Hardware and Software Analysis with Btor2C: A Word-Level-Circuit-to-C Converter
D. Beyer, P. Chien, Nian-Ze Lee
11:30
CoPTIC: Constraint Programming Translated Into C
Martin Mariusz Lester
12:00
Acacia-Bonsai: A Modern Implementation of Downset-Based LTL Realizability
Michaël Cadilhac and Guillermo Perez
FASE: Requirements, Models and AI
Chair: Facundo Molina
Room: 44-54/109
10:30
ACoRe: Automated Goal-Conflict Resolution*
Luiz Carvalho, Renzo Degiovanni, Matías Brizzio, Maxime Cordy, Nazareno Aguirre, Yves Le Traon and Mike Papadakis
11:00
Democratizing Quality-Based Machine Learning Development through Extended Feature Models
Giordano d'Aloisio, Antinisca Di Marco and Giovanni Stilo
11:30
Compositional Automata Learning of Synchronous Systems
Thomas Neele and Matteo Sammartino
12:00
Feature-Guided Analysis of Neural Networks (NIER paper)
Divya Gopinath, Luca Lungeanu, Ravi Mangal, Corina Pasareanu, Siqi Xie and Huafeng Yu
12:15
Specification and Validation of Normative Rules for Autonomous Agents (Tool paper)*
Sinem Getir Yaman, Charlie Burholt, Maddie Jones, Radu Calinescu and Ana Cavalcanti
FoSSaCS: Formal Languages
Chair:
Room: 44-45/106
10:30
Quantitative Safety and Liveness
Thomas A. Henzinger, Nicolas Mazzocchi and N. Ege Saraç
11:00
On the Comparison of Discounted-Sum Automata with Multiple Discount Factors
Udi Boker and Guy Hefetz
11:30
Fast Matching of Regular Patterns with Synchronizing Counting
Lukáš Holík, Juraj Síč, Lenka Turoňová and Tomas Vojnar
12:00
Compositional Learning for Interleaving Parallel Automata
Faezeh Labbaf, Hossein Hojjat, Jan Friso Groote and Mohammadreza Mousavi
SPIN (co-located)
Chair: Max Tschaikowski
Room: 25-26/105
11:30
Efficient Implementation of LIMDDs for Quantum Circuit Simulation
Lieuwe Vinkhuijzen, Thomas Grurl, Stefan Hillmich, Sebastiaan Brand, Robert Wille and Alfons Laarman
12:00
ParaGnosis: A Tool for Parallel Knowledge Compilation
Giso Dal, Alfons W. Laarman and Peter J.F. Lucas
12:30
Lunch
Room: Patio + Foyer
13:00
ETAPS General Assembly
Room: Auditorium
TACAS: Synthesis I
Chair: Cesar Sanchez
Room: Auditorium
14:00
Verification-guided Programmatic Controller Synthesis
Yuning Wang and He Zhu
14:30
Computing Adequately Permissive Assumptions for Synthesis
Ashwani Anand, Kaushik Mallik, Satya Prakash Nayak and Anne-Kathrin Schmuck
15:00
Taming Large Bounds in Synthesis from Bounded-Liveness Specifications
Philippe Heim and Rayna Dimitrova
15:30
Lockstep Composition for Unbalanced Loops
Ameer Hamza and Grigory Fedyukovich
ESOP: Probabilistic and Quantum Programming
Chair: Benjamin Kaminski
Room: 44-45/108
14:00
Type-safe (Variational) Quantum Programming in Idris
Liliane-Joy Dandy, Emmanuel Jeandel and Vladimir Zamdzhiev
14:30
Bunched Fuzz: Sensitivity for Vector Metrics
June Wunder, Arthur Azevedo de Amorim, Patrick Baillot and Marco Gaboardi
15:00
Fast and Correct Gradient-Based Optimisation for Probabilistic Programming via Smoothing
Basim Khajwal, Luke Ong and Dominik Wagner
15:30
Automatic Alignment in Higher-Order Probabilistic Programming Languages*
Daniel Lundén, Gizem Çaylak, Fredrik Ronquist and David Broman
FASE: Runtime Monitoring & Enforcement
Chair: Heike Wehrheim
Room: 44-54/109
14:00
Opportunistic Monitoring of Multithreaded Programs
Chukri Soueidi, Yliès Falcone and Antoine El-Hokayem
14:30
VAMOS: Middleware for Best-Effort Third-Party Monitoring
Marek Chalupa, Stefanie Muroya Lei, Fabian Muehlboeck and Thomas Henzinger
15:00
Runtime Enforcement Using Knowledge Bases
Eduard Kamburjan and Crystal Chang Din
FoSSaCS: Formal methods
Chair:
Room: 44-45/106
14:00
Pebble minimization: the last theorems
Gaëtan Douéneau-Tabot
14:30
Noetherian topologies defined via fixed-points
Aliaume Lopez
15:00
An Efficient Cyclic Entailment Procedure in a Fragment of Separation Logic
Quang Loc Le and Xuan-Bach D. Le
SPIN (co-located)
Chair: Arnd Hartmanns
Room: 25-26/105
15:00
Model Checking Futexes
Hugues Evrard and Alastair Donaldson
15:30
Sound Concurrent Traces for Online Monitoring
Chukri Soueidi and Yliès Falcone
16:00
Coffee Break
Room: Foyer + 44 lobby
SPIN (co-located)
Chair: Alfons Laarman
Room: 25-26/105
16:30
Elimination of Detached Regions in Dependency Graph Verification
Peter Gjøl Jensen, Kim Guldstrand Larsen, Jiri Srba and Nikolaj Jensen Ulrik
17:00
Potency-Based Heuristic Search with Randomness for Explicit Model Checking
Emil G. Henriksen, Alan M. Khorsid, Esben Nielsen, Theodor Risager, Jiri Srba, Adam M. Stuck and Andreas S. Sørensen
17:20
GPUexplore 3.0: GPU Accelerated State Space Exploration for Concurrent Systems with Data
Anton Wijs and Muhammad Osama
TOOLympics
Room: Auditorium
16:30
Introduction
Dirk Beyer, Fabrice Kordon, Arnd Hartmanns
16:40
CHC-COMP
Hossein Hojjat
16:46
MCC
Fabrice Kordon
16:52
QComp
Arnd Hartmanns
16:58
ARCH-COMP
Arnd Hartmanns
17:04
RERS
Falk Howar
17:10
SL-COMP
Mihaela Sighireanu
17:16
SV-COMP
Dirk Beyer
17:22
Test-Comp
Dirk Beyer
17:28
VerifyThis
Gidon Ernst
17:34
VT-LTC
Gidon Ernst
19:00
Banquet