Log in | Join us

Programme

Programme of main conferences from Monday to Thursday. Best Paper candidates are highlighted in yellow and by asterisk.

Monday Tuesday Wednesday Thursday

Monday 08 April

08:45
Opening
Room: Europe A
09:00
Lars Birkedal: Higher-Order Probabilistic Relational Separation Logic (unifying speaker)
Chair: Ana Cavalcanti
Room: Europe A
10:00
Coffee break
Room: Europe C
TACAS: SAT and SMT
Chair: Laura Kovács
Room: Hollenfels
10:30
DRAT Proofs of Unsatisfiability for SAT Modulo Monotonic Theories
Nick Feng, Alan J. Hu, Sam Bayless, Syed M. Iqbal, Patrick Trentin, Mike Whalen, Lee Pike and John Backes
11:00
Z3-Noodler: An Automata-based String Solver*
Yu-Fang Chen, David Chocholatý, Vojtěch Havlena, Lukáš Holík, Ondrej Lengal and Juraj Síč
11:15
TaSSAT: Transferring and Sharing in SAT
Md Solimul Chowdhury, Cayden Codel and Marijn Heule
11:30
Speculative SAT modulo SAT
Hari Govind Vediramana Krishnan, Isabel Garcia-Contreras, Sharon Shoham and Arie Gurfinkel
12:00
Happy ending: An empty hexagon in every set of 30 points
Marijn Heule and Manfred Scheucher
TACAS: Synthesis
Chair: Bernd Finkbeiner
Room: Diekirch-Echternach-Fischbach
10:30
Fully Generalized Reactivity(1) Synthesis
Rüdiger Ehlers and Ayrat Khalimov
11:00
Knor: reactive synthesis using Oink
Tom van Dijk, Feije van Abbema and Naum Tomov
11:30
On Dependent Variables in Reactive Synthesis
S. Akshay, Eliyahu Basa, Dror Fried and Supratik Chakraborty
12:00
CESAR: Control Envelope Synthesis via Angelic Refinements
Aditi Kabra, Jonathan Laurent, Stefan Mitsch and André Platzer
FASE: Runtime Approaches
Chair: Reiner Hähnle
Room: Schengen II
10:30
Foundations for Query-based Runtime Monitoring of Temporal Properties over Runtime Models
Lucas Sakizloglou, Holger Giese, and Leen Lambers
11:00
Probabilistic Runtime Enforcement of Executable BPMN Processes
Yliès Falcone, Gwen Salaün, and Ahang Zuo
11:30
Integrating Look-ahead Design-time and Run-time Control-synthesis for Graph Transformation Systems*
He Xu, Sven Schneider, and Holger Giese
12:00
Formal Specification of Trusted Execution Environment APIs
Geunyeol Yu, Seunghyun Chae, Kyungmin Bae, and Sungkun Moon
Rust
Room: Schengen I
10:30
Tree Borrows
Neven Villani, Johannes Hostert, Ralf Jung and Derek Dreyer
11:00
Aeneas: Rust Verification by Functional Translation
Son Ho, Jonathan Protzenko and Aymeric Fromherz
11:30
Contracts for Rust
Felix Klock and Celina Val
12:00
Building User-Friendly Rust Verification Tools
Federico Poli
12:30
Lunch
Room: Europe B
TACAS: Proof Checking
Chair: Marijn Heule
Room: Hollenfels
14:00
IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL
Hanna Lachnitt, Cesare Tinelli, Andrew Reynolds, Andres Noetzli, Haniel Barbosa, Leni Aniva, Clark Barrett and Mathias Fleury
14:30
Automate where Automation Fails: Proof Strategies for Frama-C/WP
Loïc Correnson, Allan Blanchard, Adel Djoudi and Nikolai Kosmatov
14:45
VeSCMul: Verified Implementation of S-C-Rewriting for Multiplier Verification
Mertcan Temel
15:00
A State-of-the-Art Karp-Miller Algorithm Certified in Coq
Thibault Hilaire, David Ilcinkas and Jérôme Leroux
15:30
A Logical Treatment of Finite Automata
Nishant Rodrigues, Mircea Sebe, Xiaohong Chen and Grigore Rosu
FASE: System Comprehension
Chair: Andrzej Wąsowski
Room: Schengen II
14:00
Monitoring the Future of Smart Contracts
Margarita Capretto, Martin Ceresa, and Cesar Sanchez
14:30
Comprehending Object State via Dynamic Class Invariant Learning
Jan H. Boockmann, and Gerald Luettgen
15:00
Smart Issue Detection for Large-Scale Online Service Systems Using Multi-Channel Data*
Liushan Chen, Yu Pei, Mingyang Wan, Zhihui Fei, Tao Liang, and Guojun Ma
15:30
Refinement Verification of OS Services based on a Verified Preemptive Microkernel
Ximeng Li, Shanyan Chen, Yong Guan, Qianying Zhang, Guohui Wang, and Zhiping Shi
Rust
Room: Schengen I
14:00
Verifiying a Concurrent Memory Allocator with Verus
Travis Hance
14:30
Efficiently Verifying Rust Traits with SMT Solvers
Chris Hawblitzel
15:00
OxiDD: Verification Challenge
Nils Husung, Clemens Dubslaff and Maximilian Alexander Köhl
15:30
Rust Verification Workshop Proposal: Crowdsourcing the Rust standard library verification
Celina G. Val and Rahul Kumar
Competition of Software Verification (SV-COMP)
Chair: Dirk Beyer
Room: Diekirch-Echternach-Fischbach
14:00
Introduction to SV-COMP
Dirk Beyer
14:25
Bubaak (Marek Chalupa), Bubaak-SpLit (Cedric Richter), ConcurrentWitness2Test (Levente Bajczi), CPAchecker (Daniel Baier), CPV (Po-Chun Chien)
14:45
EmergenTheta (Zsófia Ádám), ESBMC (Rafael Sá Menezes), Goblint (Michael Schwarz), Goblint Validator (Simmo Saan)
15:00
Korn (Gidon Ernst), LIV (Marian Lingsch-Rosenfeld), Mopsa (Raphaël Monat), PredatorHP (Veronika Šoková), PROTON (Ravindra Metta), SWAT (Nils Loose), Symbiotic (Jan Strejček), Theta (Csanád Telbisz)
15:30
UAutomizer (Matthias Heizmann), UGemCutter (Dominik Klumpp), UKojak (Frank Schüssele), VeriAbsL (Priyanka Darke), Witch 3 (Paulína Ayaziová), WitnessLint (Marian Lingsch-Rosenfeld)
Diversity & Inclusion
Chair: Peter Roenne
Room: Europe A
14:00
Why do we talk about Equality and Diversity in research?
Inês Crisóstomo
14:10
The Computer Girls: Exploring Herstory
Valérie Schafer
14:50
Building an Inclusive Researcher Journey
Véronique Schlick
15:00
Interactive session and discussion
16:00
Coffee break
Room: Europe C
TACAS: Logic and Decidability
Chair: Sebastian Junges
Room: Hollenfels
16:30
Answering Temporal Conjunctive Queries over Description Logic Ontologies for Situation Recognition in Complex Operational Domains
Lukas Westhofen, Christian Neurohr, Daniel Neider and Jean Christoph Jung
17:00
Deciding Boolean Separation Logic via Small Models
Tomáš Dacík, Adam Rogalewicz, Tomáš Vojnar and Florian Zuleger
17:30
Asynchronous Subtyping by Trace Relaxation
Laura Bocchi, Andy King and Maurizio Murgia
Invited Tutorial
Chair: Marieke Huisman
Room: Europe A
16:30
David Monniaux: Flavors of Abstract Interpretation
Rust
Room: Schengen I
16:30
Panel Discussion / Lightning Talks
Competition of Software Verification (SV-COMP)
Chair: Dirk Beyer
Room: Diekirch-Echternach-Fischbach
16:30
Open SV-COMP Community Meeting
Programme in PDF for print
Full Programme

ETAPS Association

Internal

Responsible for these web pages:

Jan Kofroň
Faculty of Mathematics and Physics
Charles University, Czech Republic
E-mail: firstname.lastname [at] d3s.mff.cuni.cz
Phone: +420 951 554 285