Programme
Programme of main conferences from Monday to Thursday. Distinguished papers are highlighted in yellow and by asterisk.
Wednesday 07 May
09:00
10:00
Coffee Break
TACAS: Proofs and certificates
Room:
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: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
Room:
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
Room:
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: None
Room:
10:30
INDUSTRY DAY: None
Industry Day
Room:
10:30
12:30
Lunch
13:00
ETAPS General Assembly
TACAS: Synthesis
Room:
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
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
Room:
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: None
Room:
14:00
INDUSTRY DAY: None
Industry Day
Room:
14:00
Tool demo session
Chair:
Room:
14:00
16:00
Coffee Break
TACAS: Equivalence checking
Room:
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
Room:
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
Room:
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: None
Room:
16:30
INDUSTRY DAY: None
Industry Day
Room:
16:30