Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Sun 17 Jan 2021 18:00 - 18:15 at VMCAI - Infinite-State Systems and Compilation Chair(s): Orna Grumberg

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 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

18:00 - 18:30: Infinite-State Systems and CompilationVMCAI at VMCAI
Chair(s): Orna GrumbergTechnion – Israel Institute of Technology
18:00 - 18:15
Proving the existence of fair paths in infinite state systems
Enrico MagnagoFondazione Bruno Kessler, Alberto GriggioFondazione Bruno Kessler, Alessandro CimattiFondazione Bruno Kessler
Media Attached
18:15 - 18:30
A Self-Certifying Compilation Framework for WebAssembly
Kedar NamjoshiNokia Bell Labs, Anton XueUniversity of Pennsylvania
Media Attached