Log in | Join us

Programme – Satellite Events

Programme of satellite events during the weekend.

LiVe RRRR TADM VerifyThis ASQAP EMW FMBC PLACES TLA VSS

9th Workshop on Learning in Verification (Saturday)

Saturday, May 3, Room: MDCL 1016
10:00–10:30
Coffee Break
10:30–11:30
ML and circuits at Siemens
Simon Jantsch
11:30–12:00
Formally Verified Code Generation for Solidity Smart Contracts
Jonas Schiffl, Samuel Teuber and Bernhard Beckert
12:00–12:30
Verifying Semantic Robustness in Neural Networks with Image Similarity Metrics
Jannick Strobel, David Boetius and Stefan Leue
12:30–14:00
Lunch
14:00–14:30
Neurosymbolic Automata: Improved Multimodal Reasoning versus Vision Language Models
Samuel Sasaki, Diego Manzanas Lopez and Taylor T. Johnson
14:30–15:00
Shield Synthesis for LTL Modulo Theories
Andoni Rodriguez, Felipe Gorostiaga and Cesar Sanchez
15:00–15:45
SemML + Discussion on Learning in SyntComp
Maximilian Prokop
15:45–16:30
Coffee Break

4rd Workshop on Reproducibility and Replication of Research Results (Saturday)

Saturday, May 3, Room: MDCL 1008
9:00–9:30
Security Verification Tools for Ethereum Smart Contracts: A Reusability Bonfire Story
Tommaso Oss and Carlos E. Budde
9:30–10:00
Runtime Verification Tools
Sean Kauffman and Klaus Havelund
10:00–10:30
Coffee Break
10:30–11:00
Towards a Database of Timed Automata
Nicolaj Østerby Jensen and Marius Mikučionis
11:00–11:30
Replication of (Un)sound Multi-Objective Probabilistic Model Checking Algorithms
Mark van Wijk
12:00–12:30
Bisimulation Minimisation Still Mostly Speeds Up Probabilistic Model Checking
Adnan Ahmed, Hiva Karami, Anto Nanah Ji and Franck van Breugel
11:30–12:00
MoXI: An Intermediate Language to Spur Reproducible and Comparable Model Checking Research
Kristin Yvonne Rozier
12:30–14:00
Lunch
14:00–14:30
Questioning the Centrality of Reproducibility in Scientific Evaluation
Chris Drummond
14:30–15:00
(organised by TADM)
David Parnas
15:00–16:00
Debate and discussion with audience
Chris Drummond, David Parnas, RRRR and TADM audiences
16:00–16:30
Coffee Break

International Workshop on Trusted Automated Decision-Making (Saturday)

Saturday, May 3, Room: MDCL 1110
8:45–9:00
Opening/ Welcome
Ramesh
9:00–9:30
TBA
Alan Wassyng
9:30–10:00
Neural Network Verification with Proof Production
Omri Isac
10:00–10:30
Coffee break
10:30–11:30
Never Trust Software that Imitates Intelligence! What Software Can We Trust?
David Parnas
11:30–12:00
TBA
Mark Lawford
12:00–12:30
Who Grades the Graders?
Andrés Corrada
12:30–14:00
Lunch break
14:00–14:30
Questioning the Centrality of Reproducibility in Scientific Evaluation
Chris Drummond (Jointly with RRRR)
14:30–15:00
TBA
David Parnas
15:00–16:00
Debate and discussion with audience
Chris Drummond, David Parnas, RRRR and TADM audiences
16:00–16:30
Coffee break
16:30–17:00
An Alternative Approach to Formal Mathematics
Bill Farmer
17:00–17:30
Boosted Adversarial Attacks: A Divide-and-Conquer Strategy for Revealing Vulnerabilities in Deep Learning Models
Lingyang Chu
17:30–18:00
User-Aligned Assessment of Autonomous Systems
Sandhya Saisubramanian

VerifyThis (Saturday & Sunday)

Saturday, May 3, Room: MDCL 1009
8:50–9:00
Announcements and Introduction
9:00–10:00
Challenge Session 1
10:00–10:30
Coffee Break
10:30–12:30
Team Introductions and Challenge Session 2
12:30–14:00
Lunch
14:00–16:00
Challenge Session 3 – Part 1
16:00–16:30
Coffee Break
16:30–17:30
Challenge Session 3 – Part 2
19:00–22:00
Social Dinner
Sunday, May 4, Room: MDCL 1009
9:00–18:00
Solution Discussions and Meetings with Judges

First International Workshop on Autonomous System Quality Assurance and Prediction with Digital Twins (Sunday)

Sunday, May 4, Room: MDCL 1008
9:00–9:05
Welcome + Coffee
9:05–9:25
A Case Study on the Application of Digital Twins for Enhancing CPS Operations
Irina Muntean, Mirgita Frasheri and Tiziano Munaro
9:25–9:45
BedreFlyt: Improving Patient Flows through Hospital Wards with Digital Twins
Riccardo Sieve, Paul Kobialka, Laura Slaughter, Rudolf Schlatte, Einar Broch Johnsen and Silvia Lizeth Tapia Tarifa
9:45–10:05
Verification of Digital Twins using Classical & Statistical Model Checking
Raghavendran Gunasekaran and Boudewijn Haverkort
10:05–10:30
Coffee Break
10:30–11:30
Digital twins & OTAs: How to Help Safety in Auto Industry
Mehrnoosh Askarpour
11:30–12:30
Towards Federated Digital Twin Platforms (Tool Demo paper)
Mirgita Frasheri, Prasad Talasila and Vanessa Scherma

ETAPS Mentoring Workshop (Sunday)

Sunday, May 4, Room: MDCL 1016
8:25–8:30
Welcome
Marc Frappier
8:30–9:15
Things Rarely Talked About in Academia: Failures and Management
Ina Schaefer
9:15–10:00
Descriptive and prescriptive models in formal system developments
Yamine Ait Ameur
10:00–10:30
Coffee Break
10:30–11:15
My Humble Journey Through Academia
Michael Blondin
11:15–12:00
How to Fit it All In
Marsha Chechik
12:00–12:30
Free discussions with speakers
12:30–14:00
Lunch
14:00–14:45
From Recursive Domain Equations to Reinforcement Learning for COVID
Kim Guldstrand Larsen
14:45–15:30
Building Resilience for a Research Career
Eunsuk Kang
15:30–16:00
Free discussions with speakers
16:00–16:30
Coffee Break
16:30–17:15
A Formal Methods Fellowship
Marie Farrell

6th International Workshop on Formal Methods for Blockchains (Sunday)

Sunday, May 4, Room: MDCL 1110
9:00–9:05
Welcome
Diego Marmsoler, Meng Xu
9:05–10:00
Bringing the Power of Interactive Theorem Proving to Web3
Julian Sutherland
10:00–10:30
Coffee Break
10:30–10:55
Formal Specification of Smart Contracts via Bisimulation in Coq
Derek Sorensen
10:55–11:20
Verifying Smart Contract Transformations Using Bisimulations
Kegan McIlwaine, James Caldwell
11:20–11:40
Isabell/Solidity: A tool for the Verification of Solidity Smart Contracts
Asad Ahmed, Diego Marmsoler
11:40–12:05
Formal verification in Solidity and Move: insights from a comparative analysis
Massimo Bartoletti, Silvia Crafa, Enrico Lipparini
12:05–12:30
Validity, Liquidity, and Fidelity: Formal Verification for Smart Contracts in Cardano
Tudor Ferariu, Philip Wadler, Orestis Melkonian
12:30–13:35
Lunch
13:35–14:30
Is Formal Verification Practical?
Wolfgang Grieskamp
14:30–15:00
Coffee Break
15:00–15:25
Program logics for ledgers
Orestis Melkonian, Wouter Swierstra, James Chapman
15:25–15:50
Formal Verification of a Fail-Safe Cross-Chain Bridge
Filip Maric, Bernhard Scholz, Pavle Subotić
15:50–16:15
A Readable and Computable Formalization of the Streamlet Consensus Protocol
Mauro Jaskelioff, Orestis Melkonian, James Chapman
16:15–16:40
Towards a Mechanization of Fraud Proof Games in Lean
Martin Ceresa, Cesar Sanchez
16:40–17:00
Coffee Break
17:00–17:25
ByteSpector: A Verifying Disassembler for EVM Bytecode
Franck Cassez
17:25–17:50
SCAR: Verification-based Development of Smart Contracts
Jonas Schiffl, Bernhard Beckert
17:50–18:10
A Benchmark Framework for Byzantine Fault Tolerance Testing Algorithms
João Miguel, Louro Neto, Burcu Kulahcioglu Ozkan
18:10–18:25
Closing
Diego Marmsoler, Meng Xu

Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software (Sunday)

Sunday, May 4, Room: MDCL 1116
9:05–10:00
TBA
Giovanni Bernardi
10:00–10:30
Coffee Break
10:30–11:00
Thread and Memory Safe Programming with CLASS
Luis Caires
11:00–11:30
Type Congruence, Duality and Iso-Recursive Binary Session Types
Marco Giunti and Nobuko Yoshida
11:30–12:00
Local Type Inference for Context-Free Session Types
Bernardo Almeida, Andreia Mordido and Vasco T. Vasconcelos
12:00–12:30
Capturing Happens-Before in Types
Grant Iraci, Michael Piskozub, Frank Tsai, Lukasz Ziarek and Andrew Hirsch
12:30–14:00
Lunch
14:00–14:30
AMP: Automata-based Multiparty Protocols Framework
Felix Stutz and Emanuele D'Osualdo
14:30–15:00
Separation and Encodability in Mixed Choice Multiparty Sessions
Nobuko Yoshida
15:00–15:30
Choreographies as Macros
Alexander Bohosian and Andrew K. Hirsch
15:30–16:00
An Efficient Implementation of Guard-Based Synchronization for an Object-Oriented Programming Language
Shucai Yao and Emil Sekerinski
16:00–16:30
Coffee Break
16:30–17:00
Static Communication Analysis for Hardware Design
Mads Rosendahl and Maja Hanne Kirkeby

TLA+ Community Event (Sunday)

Sunday, May 4, Room: MDCL 1115
9:00–9:15
Opening Announcements
9:15–10:00
ModelFuzz: Model guided fuzzing of distributed systems
S. Nagendra
10:00–10:30
Coffee Break
10:30–11:15
Automating Trace Validation with PGo
F. Hackett, I. Beschastnikh
11:15–12:00
Translating C to PlusCal for Model Checking of Safety Properties on Source Code
G. di Fatta, E. Ohayon, A. Methni
12:00–12:30
TLA+ for All: Model Checking in a Python Notebook
K. Läufer, G.K. Thiruvathukal
12:30–14:00
Lunch
14:00–14:45
Formal models for monotonic pipeline architectures
J.-P. Bodeveix, A. Bonenfant, T. Carle, M. Filali, C. Rochange
14:45–15:30
TLA+ Modeling of MongoDB Transactions
M. Demirbas, W. Schultz
15:30–16:00
Are We Serious About Using TLA+ For Statistical Properties?
A. Jesse Jiryu Davis
16:00–16:30
Coffee Break
16:30–17:00
It's never been easier to write TLA+ tooling!
A. Helwer
17:00–17:30
Discussion panel and closing remarks

International Workshop on Verification of Scientific Software (Sunday)

Sunday, May 4, Room: MDCL 1010
9:00–10:00
Foundational end-to-end verification of numerical programs (Keynote talk)
Andrew Appel
10:00–10:30
Coffee Break
10:30–11:00
Towards Richer Challenge Problems for Scientific Computing Correctness
Matthew Sottile, Mohit Tekriwal, and John Sarracino
11:00–11:30
Verifying a Sparse Matrix Algorithm Using Symbolic Execution
Alex Wilton
11:30–12:00
Mechanizing Olver’s Error Arithmetic
Max Fan, Ariel E. Kellison, and Samuel D. Pollard
12:00–12:30
Property Testing for Ocean Models. Can We Specify It?
Deepak Cherian
12:30–14:00
Lunch
14:00–14:45
Automated Program Analysis for Scientific Software (Keynote talk)
Jacob Laurel
14:45–15:15
Fast Trigonometric Functions using the RLIBM Approach
Sehyeok Park and Santosh Nagarakatte
15:15–15:45
Specification and Verification for Climate Modeling: Formalization Leading to Impactful Tooling
Alper Altuntas, Allison H. Baker, Ganesh Gopalakrishnan, John Baugh, and Stephen Siegel
15:45–16:00
Introduction to Challenge Problems
Stephen Siegel
16:00–16:30
Coffee Break
16:30–17:00
Challenge Problem Presentations
various
Main 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