Generation of polynomial inequalities as invariants

摘要: Embedded software in critical systems rise a need for analysis, especially guaranteeing safety properties. In the late seventies, Cousot & introduced general framework, called abstract interpretation, dedicated to conception of particular analyses: static analyses. Among program properties interest, discovering algebraic relationships between variables allows proving lack run-time errors. While inference linear is e fficiently solved, computing polynomial equalities as invariants still challenge, fortiori inequality counterpart. After brief overview existing techniques invariant inference, this report investigates viability constraint-based method inequalities invariants.