Program
Program
| Time | 25 November 2024 | 26 November 2024 | ||
|---|---|---|---|---|
| Room1: CS209 | Room2: CS210 | Room1: CS209 | Room2: CS210 | |
| 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 @AITCC Dining Room | |||
| 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 at 15:30 with bus in front of AITCC | |
| 18:00 – 21:30 | Dinner @AIT or nearby restaurant | Reception @The Lounge 10th Floor, Berkeley Hotel | ||
Program
| Time | 27 Nov 2024 | 28 Nov 2024 | 29 Nov 2024 |
|---|---|---|---|
| Kensington 5th Floor, Berkeley Hotel | Kensington 5th Floor, Berkeley Hotel | Kensington 5th Floor, Berkeley Hotel | |
| 08:45-9:00 | Conference Opening | ||
| 9:00-10:00 | Invited Speaker 1: (Chair: Zhiming Liu) Proving Safety of Automated Driving Vehicles Ichiro Hasuo | Invited Speaker 3: (Chair: Ichiro Hasuo) The Unreasonable Effectiveness of Automated Reasoning in Quantum Computing Alfons Laarman | Invited Speaker 4: (Chair: Alfons Laarman) Automated Synthesis: Fusing Formal Methods and AI Priyanka Golia |
| Break | Break | Break | |
| 10:30-12:00 | Session 1a: Automata, Languages, and Learning (Chair: Martin Leucker) 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 Well-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny Stefan Zetzsche and Wojciech Różowski | Session 4: Process Calculi (Chair: Annabelle Mclver) 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 (Chair: Fabio Zanasi) 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: (Chair: Emil Sekerinski) Probabilistic Datatypes Annabelle McIver | Session 2b: Algorithms and Complexity (Chair: Tim Copperman) 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 (Chair: Uwe Nestmann) 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 (Chair: Emil Sekerinski) 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 (Chair: Burkhart Wolff) 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 (Chair: Priyanka Golia) 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: 01/12/2024