Room 206 (2nd floor, badged access)
12 November 2026 - 14h00
The existence of polyhedral invariants is undecidable for linear systems
by David Monniaux from CNRS - VERIMAG
Abstract: The existence of polyhedral inductive invariants suitable for proving that a given control location is unreachable is undecidable for programs using only linear arithmetic over integers or rationals, by reduction from 2-counter machines.
