Proving the existence of fair paths in infinite state systems
In finite-state systems, true existential properties admit witnesses in form of lasso-shaped fair paths. When dealing with the infinite-state case (e.g. software non-termination, model checking of hybrid automata) this is no longer the case. In this paper, we propose a compositional approach for proving the existence of fair paths of infinite-state systems. First, we describe a formal approach to prove the existence of a non-empty under-approximation of the original system that only contains fair paths. Second, we define an automated procedure that, given a set of hints (in form of basic components), searches for a suitable composition proving the existence of a fair path. We experimentally evaluate the approach on examples taken from both software and hybrid systems, showing its wide applicability and expressiveness.
Sun 17 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
18:00 - 18:30
|Proving the existence of fair paths in infinite state systems|
Enrico Magnago Fondazione Bruno Kessler, Alberto Griggio Fondazione Bruno Kessler, Alessandro Cimatti Fondazione Bruno KesslerMedia Attached
|A Self-Certifying Compilation Framework for WebAssembly|