ACV — PROGRAM
Days: Friday, 24 July 2026 Saturday, 25 July 2026
Friday, 24 July 2026
09:00-09:15
opening
ACV
Location:
C4.07
09:15-10:30
24am1
ACV
Location:
C4.07
| 09:15-10:00 |
tba (Invited Talk) (abstract) 45 min
1 Saarland University and University College London
|
| 10:00-10:30 |
Certified Harmonic-Mean Abstraction and Refinement for Continuous-Time Markov Chains (abstract) 30 min
1 Utah State University
2 ENS Paris-Saclay
3 University of Colorado Boulder
|
10:30-11:00
Coffee Break
ACV
Location:
C4.07
11:00-12:00
24am2
ACV
Location:
C4.07
| 11:00-11:30 |
Constrained and Robust Policy Synthesis with Satisfiability-Modulo-Probabilistic-Model-Checking (abstract) 30 min
1 Radboud University
2 Brno University of Technology
|
| 11:30-12:00 |
Stochastic Processes: Coinduction in Probabilistic Programming (abstract) 30 min
1 University of Oxford
|
12:00-14:00
Lunch
ACV
Location:
C4.07
14:00-15:30
24pm1
ACV
Location:
C4.07
| 14:00-14:30 |
Robust Probabilistic Bisimilarity (Invited Talk) (abstract) 30 min
1 University of Oxford
|
| 14:30-15:00 |
SV-LIB 1.0: A Standard Exchange Format for Software-Verification Tasks (abstract) 30 min
1 LMU Munich
|
| 15:00-15:30 |
Imprecise Probabilistic Programming, Precisely (abstract) 30 min
1 University of Oxford
|
15:30-16:00
Coffee Break
ACV
Location:
C4.07
16:00-18:00
24pm2
ACV
Location:
C4.07
| 16:00-16:30 |
A Lattice-Theoretic Abstraction of PDR via Adjunctions (Invited Talk) (abstract) 30 min
1 Kyoto University
|
| 16:30-17:00 |
Multiobjective Predicate Transformers: Computing the Pareto Front in Probabilistic Programs (abstract) 30 min
1 Cornell University
2 RWTH Aachen University
3 Radboud University
4 Saarland University and University College London
5 Saarland University and RWTH Aachen University
|
| 17:00-17:30 |
Verification of Systems with Unbounded Agents By Exploiting Concurrency (abstract) 30 min
1 Unaffiliated
|
| 17:30-18:00 |
Scalable Probabilistic Program Verification by Theory-Extended Decision Diagrams (abstract) 30 min
1 RWTH Aachen University
2 University of Münster
3 Radboud University
|
Saturday, 25 July 2026
09:00-09:45
25am1-1
ACV
Location:
C4.07
| 09:00-09:45 |
Type Systems for Exchangeability (Invited Talk) (abstract) 45 min
1 Cornell University
|
09:45-10:00
(mini-break for changing rooms)
ACV
Location:
C4.07
10:00-10:30
25am1-2
ACV
Location:
C4.07
| 10:00-10:30 |
Coalgebraic Notions of Simulation, Bisimulation and Relators (abstract) 30 min
1 University of Birmingham
|
10:30-11:00
Coffee Break
ACV
Location:
C4.07
11:00-12:00
25am2
ACV
Location:
C4.07
| 11:00-11:30 |
Compositional Verification of Higher-Order Effectful Programs via Interactive Semantics (abstract) 30 min
1 Nantes Université
|
| 11:30-12:00 |
Why codensity lifting works: A formal perspective (abstract) 30 min
1 University of Oxford
|
12:00-14:00
Lunch
ACV
Location:
C4.07
14:00-15:30
25pm1
ACV
Location:
C4.07
| 14:00-14:45 |
tba (Invited Talk) (abstract) 45 min
1 INRIA
|
| 14:45-15:30 |
An equational axiomatization of dynamic threads (Invited Talk) (abstract) 45 min
1 University of Birmingham
|
15:30-16:00
Coffee Break
ACV
Location:
C4.07
16:00-17:45
25pm2
ACV
Location:
C4.07
| 16:00-16:45 |
Approximative Fixpoint Theory and Applications to Reinforcement Learning (Invited Talk) (abstract) 45 min
1 University of Duisburg-Essen
|
| 16:45-17:15 |
Semantics and Equational Axiomatisation of Quantum Communication (abstract) 30 min
1 University of Oxford
|
| 17:15-17:45 |
Basic Lattice Theory for Basic Model Checking (abstract) 30 min
1 National Institute of Informatics
|