PROGRAM
Days: Monday, September 7th Tuesday, September 8th Wednesday, September 9th Thursday, September 10th Friday, September 11th
Monday, September 7th
View this program: with abstractssession overviewtalk overview
09:00-10:30 Session 1: Tutorial 1 - Part 1
| 09:00 | TBA - Part 1 |
11:00-12:30 Session 2: Tutorial 1 - Part 2
| 11:00 | TBA - Part 2 |
14:30-16:00 Session 3: Tutorial 2 - Part 1
| 14:30 | TBA - Part 1 |
16:30-18:00 Session 4: Tutorial 2 - Part 2
| 16:30 | TBA - Part 2 |
Tuesday, September 8th
View this program: with abstractssession overviewtalk overview
10:30-12:06 Session 6A: Presentations
| 10:30 | Automata for MSO over Infinite Trees with Quantification over Borel Sets of Branches (abstract) |
| 10:42 | Layered automata: A canonical model for automata over infinite words (abstract) |
| 10:54 | History-deterministic Büchi automata are succinct (abstract) |
| 11:06 | A simple algorithmic framework for disambiguation of finite automata (abstract) |
| 11:18 | Decomposition of Automata recognizing Ideals (abstract) |
| 11:30 | Regular Languages Out of Order: An Algebraic View of Streaming Space (abstract) |
| 11:42 | Asymptotic Hausdorff and Language Similarity (abstract) |
| 11:54 | Hierarchical-Alphabet Automata: Extendable Acceptors for Languages of Nested Words (abstract) |
| 12:06 | Computing Measures: Fixed Points Beyond Lattices (abstract) |
10:30-12:06 Session 6B: Presentations
| 10:30 | Dicey Games: Shared Sources of Randomness in Distributed Systems (abstract) |
| 10:42 | Verification of Equilibria in Probabilistic Concurrent Multiplayer Reachability Games (abstract) |
| 10:54 | Don't Start From Zero: Optimizing Value Iteration in MDPs After Action Removal (abstract) |
| 11:06 | Tractable Hyperproperties for MDPs (abstract) |
| 11:18 | Sure-almost-sure Window Mean Payoff in Markov Decision Processes (abstract) |
| 11:30 | Stopping Criterion for Strategy Improvement on Concurrent Stochastic Games (abstract) |
| 11:42 | Randomise Alone, Reach as a Team (CAV26 Paper) (abstract) |
| 11:54 | Revealing POMDPs: Qualitative and Quantitative Analysis for Parity Objectives (abstract) |
14:30-16:00 Session 7A: Presentations
| 14:30 | Representations: a general theory (abstract) |
| 14:42 | Program Logics via Distributive Monoidal Categories (abstract) |
| 14:54 | The Magmoid of Normalized Stochastic Kernels (abstract) |
| 15:06 | Languages and Recognition in a Category with Factorisation (abstract) |
| 15:18 | Polynomial Algebras of Logical Structures (abstract) |
| 15:30 | Register Automata in a Category (abstract) |
| 15:42 | Alternating Kleene Algebra (abstract) |
14:30-16:00 Session 7B: Presentations
| 14:30 | Opacity problems in multi-energy timed automata (abstract) |
| 14:42 | Best-Effort Safety Control of Multi-Mode Systems (abstract) |
| 14:54 | (In)aproximability of weighted timed games (abstract) |
| 15:06 | Scalable Current-State Estimation of Discrete-Timed Automata (abstract) |
| 15:18 | Back in Time: Bringing a Classical Theory of Compositional Verification to Timed Automata (abstract) |
| 15:30 | Efficiently computable temporal robustness for a practical STL fragment (abstract) |
Wednesday, September 9th
View this program: with abstractssession overviewtalk overview
10:30-12:30 Session 9A: Presentations
| 10:30 | From Sets to Points: Simplifying MSO Interpretations via Reparameterizations (abstract) |
| 10:42 | On Variable-Bounded Non-Linear Expansions of Presburger Arithmetic (abstract) |
| 10:54 | Interpolants in Modal Logic with Nominals (abstract) |
| 11:06 | Complexity of Clique-Guarded First-Order Logic with Counting (abstract) |
| 11:18 | Hereditary 2-WQO Graph Classes Have Bounded Clique-Width (abstract) |
| 11:30 | Order-invariant cluster first-order logic on graph classes of bounded degree (abstract) |
| 11:42 | Join Queries with Insertion Order: Expressiveness and Query Evaluation (abstract) |
| 11:54 | Extending MSO with index quantifiers (abstract) |
| 12:06 | Alice, Bob, and Finite Relational Structures (abstract) |
10:30-12:30 Session 9B: Presentations
| 10:30 | The complexity of downward closures of indexed languages (abstract) |
| 10:42 | The Complexity of Nested Reset Counter Systems (abstract) |
| 10:54 | The complexity of well-matched regularity for visibly pushdown languages (abstract) |
| 11:06 | Quantitative Analysis of Pushdown Networks (abstract) |
| 11:18 | Bounded treewidth, multiple context-free grammars, and downward closures (abstract) |
| 11:30 | Extending VASS with Additional Integer Counters (abstract) |
| 11:42 | Exploring VASS Parameterised by Geometric Dimension (abstract) |
| 11:54 | Integer reachability in data VASS (abstract) |
| 12:06 | Reachability in Branching Vector Addition Systems (abstract) |
Thursday, September 10th
View this program: with abstractssession overviewtalk overview
10:30-12:30 Session 12A: Presentations
| 10:30 | Preservation Theorems for Transducer Outputs (abstract) |
| 10:42 | Edit Distance of Finite-Valued Transducers (abstract) |
| 10:54 | Hamming distance between finite transducers (abstract) |
| 11:06 | String Solving with Stabilization and Transducers (abstract) |
| 11:18 | Towards an Equational Theory for String-to-String Regular Functions (abstract) |
| 11:30 | Reducing tree logic membership problems to automata-theoretic membership problems (abstract) |
| 11:42 | Tree Automata Acceptance up to Measurable Defect (abstract) |
| 11:54 | Ultimately-cyclic equational systems (abstract) |
| 12:06 | Lasso games (abstract) |
| 12:18 | Van der Put Coefficients and Automata (abstract) |
10:30-12:30 Session 12B: Presentations
| 10:30 | On the Subspace Orbit Problem and the Simultaneous Skolem Problem (abstract) |
| 10:42 | Kannan and Lipton meet Schanuel (abstract) |
| 10:54 | Fine-Grained Complexity of XNFA and NFA Acceptance (abstract) |
| 11:06 | Algebraic and algorithmic methods for computing polynomial loop invariants (abstract) |
| 11:18 | Non-negative residual functions (abstract) |
| 11:30 | Parallel Abstract Interpretation for Polynomial Programs with Range Bound Assertions (abstract) |
| 11:42 | On Deciding Constant Runtime of Linear Loops (abstract) |
| 11:54 | Foundations for Deductive Verification of Continuous Probabilistic Programs (abstract) |
| 12:06 | Pumping Sequence Families (abstract) |
| 12:18 | Revisiting Finiteness of Matrix Monoids (abstract) |
14:30-16:00 Session 13A: Presentations
| 14:30 | Transformers are Inherently Succinct (abstract) |
| 14:42 | Scalable Learning of One-Counter Automata via State-Merging Algorithms (abstract) |
| 14:54 | Formalism and Learning of Visibly Recursive Automata (abstract) |
| 15:06 | Follow the STARs: Dynamic ω-Regular Shielding of Learned Probabilistic Policies (abstract) |
| 15:18 | Strategy Repair on Parity Games using Semantic Information and Machine Learning (abstract) |
| 15:30 | Expectation Bounds and Termination for Programs with Unbounded Updates (abstract) |
| 15:42 | Beep is all you need (abstract) |
| 15:54 | Population Protocols over Ordered Agents (abstract) |
14:30-16:00 Session 13B: Presentations
| 14:30 | Towards a Parallel Knowledge Compilation Map (abstract) |
| 14:42 | Multi-Player Discrete-Bidding Games (abstract) |
| 14:54 | Bidding Games with Income: Reachability in the Discrete poorman Setting (abstract) |
| 15:06 | Cellular Automata as Language Generators: Gliders Beyond Regularity (abstract) |
| 15:18 | Maximizing Independence in Auction-Based Scheduling via Successive Refinement (abstract) |
| 15:30 | Belief Entropy as a Risk Dial: Wasserstein-Robust Bellman Equations for Safe Sequential Decision Making} (abstract) |
| 15:42 | Runtime Monitoring of DNNs via Randomised Smoothing (abstract) |
Friday, September 11th
View this program: with abstractssession overviewtalk overview
09:00-10:00 Session 14: Invited Talk
| 09:00 | Understanding Transformers through the Lens of Logic and Automata (abstract) |
10:30-12:30 Session 15A: Presentations
| 10:30 | Infinite-state games with energy objectives beyond counters (abstract) |
| 10:42 | An Automata-Based Approach to Games with ω-Automatic Preferences (abstract) |
| 10:54 | Decoupled Planning for Multiple Omega-Regular Objectives (abstract) |
| 11:06 | A Conway-universal automaton for structurally Adam-positional automata (abstract) |
| 11:18 | Memory requirements of omega-regular objectives: from deterministic to stochastic games (abstract) |
| 11:30 | Playing Against a Partially-Known Opponent (abstract) |
| 11:42 | Games on Higher Dimensional Automata (abstract) |
| 11:54 | A Parameterized Büchi-Landweber Theorem (abstract) |
10:30-12:30 Session 15B: Presentations
| 10:30 | Runtime Consultants (abstract) |
| 10:42 | Symbolic omega-automata with obligations (abstract) |
| 10:54 | Distance between interval pomsets with interface (abstract) |
| 11:06 | Lagrangian-Based Duality for Quantified SMT Algorithms (abstract) |
| 11:18 | Lean on Vampire Proofs (abstract) |
| 11:30 | Deciding Separation Logic with Inductive Definitions via Translation to SMT (abstract) |
| 11:42 | PETRIFY- Concurrent program analysis using Petri Nets (abstract) |
| 11:54 | Reasoning about Parameterized Quantum Circuits using Tree Automata (abstract) |