(un)decidability of polyhedral invariant inference

Is the existence of polyhedral inductive invariants decidable?

Polyhedral invariants have long been used in static program analysis, and are either computed in restricted classes of polyhedra, or obtained through heuristics, as though it were impossible to find a general algorithm for finding such invariants.

There have been attempts at proving that no such algorithm exists. The goal of this internship is to think further about the issue.


Contact | Site Map | Site powered by SPIP 4.2.16 + AHUNTSIC [CC License]

info visites 4214996