Programme
Programme of main conferences from Monday to Thursday. Distinguished papers are highlighted in yellow and by asterisk.
Wednesday 07 May
09:00
Amal Ahmed (ESOP invited speaker)
Chair: Viktor Vafeiadis
Room: MDCL 1305
10:00
Coffee Break
Room: MDCL
TACAS: Proofs and certificates
Chair: Daniela Kaufmann
Room: MDCL 1102
10:30
Unsatisfiability Proofs for Horn Solving*
Rodrigo Otoni, Martin Blicha, Matias Barandiaran Rivera, Patrick Eugster, Jan Kofroň and Natasha Sharygina
11:00
Fixed Point Certificates for Reachability and Expected Rewards in MDPs
Krishnendu Chatterjee, Tim Quatmann, Maximilian Schäffeler, Maximilian Weininger, Tobias Winkler and Daniel Zilken
11:15
11:30
Certifying Pareto-Optimality in Multi-Objective Maximum Satisfiability
Christoph Jabs, Jeremias Berg, Bart Bogaerts and Matti Järvisalo.
12:00
Revisiting DRUP-based Interpolants with CaDiCaL 2.0
Yakir Vizel and Basel Khouri
ESOP: Semantics
Chair: Marieke Huisman
Room: MDCL 1305
10:30
Coverage Semantics for Dependent Pattern Matching
Joseph Eremondi and Ohad Kammar
11:00
An abstract, certified account of operational game semantics
Peio Borthelle, Guilhem Jaber, Tom Hirschowitz and Yannick Zakowski
11:30
Context-Dependent Effects in Guarded Interaction Trees
Sergei Stepanenko, Emma Nardino, Dan Frumin, Amin Timany and Lars Birkedal
12:00
On the Relationship between Dijkstra Monads and Higher-Order Fixpoint Logic*
Risa Yamada, Naoki Kobayashi, Ken Sakayori and Ryosuke Sato
FOSSACS: Time and Concurrency
Chair: Eduardo Bonelli
Room: MDCL 1105
10:30
Model-checking real-time systems: revisiting the alternating automaton route*
Patricia Bouyer, B Srivathsan and Vaishnavi Vishwanath
11:00
Temporal Hyperproperties for Population Protocols
Nicolas Waldburger, Chana Weil-Kennedy, Pierre Ganty and César Sánchez
11:30
Structural Liveness of Conservative Petri Nets (Complexity, petri nets, structural liveness)
Petr Jancar, Jérôme Leroux and Jiri Valusek
12:00
Two-sorted algebraic decompositions of Brookes's shared-state denotational semantics (Models, axiomatization, effects)
Yotam Dvir, Ohad Kammar, Ori Lahav and Gordon Plotkin
SPIN
Room: MDCL 1009
10:30–11:30
Developments in Symbolic Model Checking
Orna Grumberg
11:30–12:00
Accelerating CAR-based Model-Checking with Multiple Unsatisfiable Cores
Yibo Dong, Xiwei Wu, Jianwen Li, Geguang Pu and Ofer Strichman
12:00–12:30
Efficient Model Checking for the Alternating-Time µ-Calculus via Effectivity Frames
Daniel Hausmann, Merlin Humml, Simon Prucker and Lutz Schröder
INDUSTRY DAY
Room: MDCL 1110
10:30
Weathering the Weather: The Storms Gathering Around the Development of Safety-Critical Systems
Chris Hobbs (Consultant)
11:15
Safe Agile: A Safety Strategy for Agile Development Strategy for Spacecrafts or Space robots
Thomas Chowdhury (MDA Space)
12:00
Temporal specification languages in industrial hardware verification
Simon Jantsch (Siemens EDA)
12:30
Lunch
Room: CIBC Hall & Foyer
13:00
ETAPS General Assembly
Room: MDCL 1305
TACAS: Synthesis
Chair: Elizabeth Polgreen
Room: MDCL 1102
14:00
Accelerating Protocol Synthesis and Detecting Unrealizability with Interpretation Reduction
Derek Egolf and Stavros Tripakis
14:30
Synthesis of Universal Safety Controllers
Bernd Finkbeiner, Niklas Metzger, Satya Prakash Nayak and Anne-Kathrin Schmuck
14:45
15:00
Synthesis with Guided Environments
Orna Kupferman and Ofer Leshkowitz
15:30
Value Iteration with Guessing for Markov Chains and Markov Decision Processes
Krishnendu Chatterjee, Mahdi Jafariraviz, Raimundo Saona Urmeneta and Jakub Svoboda
ESOP: Concurrency 1
Chair: Viktor Vafeiadis
Room: MDCL 1305
14:00
Iso-Recursive Multiparty Sessions and their Automated Verification
Marco Giunti and Nobuko Yoshida
14:30
Multiparty Session Types with a Bang!
Matthew Alan Le Brun, Simon Fowler and Ornela Dardha
15:00
First-Person Choreographic Programming with Continuation-Passing Communications*
Sung-Shik Jongmans
15:30
An Automata-theoretic Basis for Specification and Type Checking of Multiparty Protocols
Felix Stutz and Emanuele D'Osualdo
SPIN
Room: MDCL 1009
14:00
MoXI session
INDUSTRY DAY
Room: MDCL 1110
14:00
The Challenge of Information Management within the Software Defined Vehicles
Tara Vatcher (Stellantis)
14:45
Using lightweight formal methods to check correctness of production code for Amazon S3
Rajeev Joshi (Amazon Web Services)
15:30
Abstract Interpretation of Floating-Point Digital Filters in Nuclear Plant Software.
Pierre-Yves Piriou (EDF), Maxime Jacquemin (CEA) and Franck Védrine (CEA)
Tool Demo Session
Chair:
Room: MDCL 1008
14:00
16:00
Coffee Break
Room: MDCL
TACAS: Equivalence checking
Chair: Anton Wijs
Room: MDCL 1102
16:30
Refuting Equivalence in Probabilistic Programs with Conditioning
Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Petr Novotný and Đorđe Žikelić
17:00
Revisiting Differential Verification: Equivalence Verification with Confidence
Samuel Teuber, Philipp Kern, Marvin Janzen and Bernhard Beckert
17:30
Equivalence Checking of a libm Port
Mark S. Baranowski, Zvonimir Rakamaric and Ganesh Gopalakrishnan.
ESOP: Fresh Perspectives
Chair: Peter Müller
Room: MDCL 1305
16:30
Neural Network Verification is a Programming Language Challenge
Lucas C. Cordeiro, Matthew L. Daggitt, Julien Girard-Satabin, Omri Isac, Taylor T. Johnson, Guy Katz, Ekaterina Komendantskaya, Augustin Lemesle, Edoardo Manino, Artjoms Šinkarovs and Haoze Wu
17:00
Formal Autograding in a Classroom
Dragana Milovančević, Mario Bucev, Marcin Wojnarowski, Samuel Chassot and Viktor Kunčak
17:30
The Vanilla Sequent Calculus is Call-by-Value
Beniamino Accattoli
FOSSACS: Programs
Chair: Naoki Kobayashi
Room: MDCL 1105
16:30
Sharing and Linear Logic with Restricted Access*
Pablo Barenbaum and Eduardo Bonelli
17:00
Combining quantum and classical control: syntax, semantics and adequacy
Kinnari Dave, Louis Lemonnier, Romain Péchoux and Vladimir Zamdzhiev
17:30
BiGKAT: an algebraic framework for relational verification of probabilistic programs
Leandro Gomes, Patrick Baillot and Marco Gaboardi
SPIN
Room: MDCL 1009
16:30
0-1 Laws for LTL and CTL over Random Transition Systems
Yanni Dong, Milan Lopuhaä-Zwakenberg and Marielle Stoelinga
17:00
A Modular Program-Transformation Framework for Reducing Specifications to Reachability
Dirk Beyer, Marek Jankola, Marian Lingsch-Rosenfeld, Tian Xia and Xiyue Zheng
17:30
(Asynchronous) Temporal Logics for Hyperproperties on Finite Traces
Alberto Bombardelli, Laura Bozzelli, Cesar Sanchez and Stefano Tonetta
INDUSTRY DAY
Room: MDCL 1110
16:30
Advancing software solutions for CAR-T therapy manufacturing and standardization.
Ethan Dhanraj (OmniaBio) and Hanene Ben Yedder (OmniaBio)
17:00
Agile Development: Ensuring Safety in Rapid Iteration Cycles
Mehrnoosh Askarpour (General Motors Canada), Sahar Kokaly (General Motors Canada) and Ramesh S (General Motors R&D)
17:30
Networking and informal discussions
18:30
Banquet
Room: LIUNA Station