Program
Program
| Time | 25 November 2024 | 26 November 2024 | ||
|---|---|---|---|---|
| 08:45 – 09:00 | Tutorial Opening | Tutorial Opening | ||
| 09:00 – 10:00 | Tutorial 1: An introduction to Runtime Verification Martin Leucker |
Training 1: SAT Solvers: Modern Approaches and Applications |
Tutorial 3: Quantum Circuit Compilation using Formal Methods | Training 3: A Formal Look at Programming Emil Sekerinski |
| 10:00 – 10:30 | Break | |||
| 10:30 – 12:00 | Tutorial 1 (cont.): Martin Leucker | Training 1 (cont.): Priyanka Golia | Tutorial 3 (cont.): Alfons Laarman & Tim Coopmans | Training 3 (cont.): Emil Sekerinski |
| 12:00 – 13:30 | Lunch | |||
| 13:30 – 15:00 |
Tutorial 2: Abstract and Concrete Model Checking: Through the Lens of Lattice Theory and Category Theory |
Training 2: Formal Aspects of Model-Driven Development — A Unified Method |
Tutorial 4: ProofBuddy: A Gentle Online Proof Assistant for Learners | |
| 15:00 – 15:30 | Break | |||
| 15:30 – 17:00 | Tutorial 2 (cont.): Ichiro Hasuo | Training 2 (cont.): Zhiming Liu | Travel to Bangkok | |
| 18:00 – 21:30 | Dinner @AIT or nearby restaurant | Reception @Berkeley Hotel | ||
Program
| Time | 27 Nov 2024 | 28 Nov 2024 | 29 Nov 2024 |
|---|---|---|---|
| 08:45-9:00 | Conference Opening | ||
| 9:00-10:00 | Invited Speaker 1: Proving Safety of Automated Driving Vehicles Ichiro Hasuo | Invited Speaker 3: The Unreasonable Effectiveness of Automated Reasoning in Quantum Computing Alfons Laarman | Invited Speaker 4: Automated Synthesis: Fusing Formal Methods and AI Priyanka Golia |
| Break | Break | Break | |
| 10:30-12:00 | Session 1a: Automata, Languages, and Learning Well-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny Stefan Zetzsche and Wojciech Różowski Jump Complexity of Deterministic Finite Automata with Translucent Letters Szilárd Zsolt Fazekas, Victor Mitrana, Andrei Păun and Mihaela Păun Learning Closed Signal Flow Graphs Ekaterina Piotrovskaya, Leo Lobski and Fabio Zanasi | Session 4: Process Calculi Reversibility in Process Calculi with Nondeterminism and Probabilities Marco Bernardo and Claudio Antares Mezzina A Theory of Proc-Omata — and a Proof Technique for Parameterized Process Architectures Benoît Ballenghien and Burkhart Wolff Formal Foundations for Efficient Simulation of MOM Systems Sini Chen, Huibiao Zhu, Ran Li, Lili Xiao, Jiapeng Wang, Ning Ge and Xinbin Cao | Session 1b: Automata, Languages, and Learning Dual Adjunction Between Ω-Automata and Wilke Algebra Quotients Anton Chernev, Helle Hvid Hansen and Clemens Kupke On Concurrent Program Algebra and Demonic Automata Emil Sekerinski Bisimulations and Logics for Higher-Dimensional Automata Safa Zouari, Uli Fahrenberg and Krzysztof Ziemianski |
| Lunch | Lunch | Lunch | |
| 13:30-14:30 | Invited Speaker 2: Probabilistic Datatypes Annabelle McIver | Session 2b: Algorithms and Complexity Generalized Parikh Matrices For Tracking Subsequence Occurrences Szilárd Zsolt Fazekas and Xinhao Huang Card-Based Protocols with Single-Card Encoding Kazumasa Shinagawa | Session 5a: Verification and Reasoning Verifying Type Safety for Isabelle/Solidity Billy Thornton and Diego Marmsoler History-Based Reasoning about Behavioral Subtyping Jinting Bian, Hans-Dieterh Hiep and Frank de Boer Switched Systems in Coq for Modeling Periodic Controllers Andrei Aleksandrov and Kim Völlinger |
| 14:30-15:00 | Session 2a: Algorithms and Complexity Runtime Enforcement with Event Reordering Ankit Pradhan, C G Mitun Akil and Srinivas Pinisetty Maximizing Weighted Dominance in the Plane Waseem Akram and Sanjeev Saxena | Visit to Ayutthaya (Wat Phra Si Sanphet & Wat Mahathat) | |
| Break | Break | ||
| 15:30-17:00 | Session 3: Graphs and Games Winning Strategy Templates for Stochastic Parity Games towards Permissive and Resilient Control Kittiphon Phalakarn, Sasinee Pruekprasert and Ichiro Hasuo Disconnection Rules are Complete for Chemical Reactions Leo Lobski, Fabio Zanasi and Ella Gale Verification with Common Knowledge of Rationality for Graph Games Rindo Nakanishi, Yoshiaki Takata and Hiroyuki Seki | Session 5b: Verification and Reasoning Automated proof of Ramsey theorem via symbolic computation Zhenbing Zeng, Jian Lu and Liangyu Chen Runtime Enforcement with Event Reordering Ankit Pradhan, C G Mitun Akil and Srinivas Pinisetty | |
| Closing | |||
| 18:00-21:30 | Dinner @Grand Chao Praya Riverside |
(Update 24/09/2024)