VMCAI 2026
Mon 12 - Tue 13 January 2026 Rennes, France
co-located with POPL 2026
Mon 12 Jan 2026 17:00 - 17:30 at Horizons - Models 1 Chair(s): Mihaela Sighireanu

Identifying the actual cause of events in engineered systems is a fundamental challenge in system analysis. Finding such causes becomes more challenging in the presence of noise and stochastic behavior in real-world systems. In this paper, we adopt the notion of probabilistic actual causality by Fenton-Glynn, which is a probabilistic extension of Halpern and Pearl’s actual causality, and propose a novel method to formally reason about causal effect of events in stochastic systems. We (1) formulate the discovery of probabilistic actual causes in computing systems as an SMT problem, and (2) address the scalability challenges by introducing an abstraction-refinement technique that improves efficiency by up to 95%. We demonstrate the effectiveness of our approach through three case studies, identifying probabilistic actual causes of safety violations in (1) the Mountain Car problem, (2) the Lunar Lander benchmark, and (3) MPC controller for an F-16 autopilot simulator.

Mon 12 Jan

Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

16:00 - 17:30
Models 1VMCAI 2026 at Horizons
Chair(s): Mihaela Sighireanu University Paris-Saclay, ENS Paris-Saclay, CNRS, LMF
16:00
30m
Talk
Verification of Generic VHDL Designs and Their Translation to Rocq
VMCAI 2026
Ocan Sankur University of Rennes, France / Inria, France / CNRS, France / IRISA, France, Benoît Boyer Mitsubishi Electric R&D Centre Europe, Rennes, France, Florian Faissole Mitsubishi Electric R&D Centre Europe
16:30
30m
Talk
A Formal Executable Semantics of PROMELADistinguished Paper
VMCAI 2026
Byoungho Son POSTECH, Kyungmin Bae POSTECH
17:00
30m
Talk
Efficient Discovery of Actual Causality in Stochastic Systems
VMCAI 2026
Arshia Rafieioskouei Michigan State University, Kenneth Rogale Michigan State University, Borzoo Bonakdarpour Michigan State University