Generation of polynomial inequalities as invariants - DUMAS - Dépôt Universitaire de Mémoires Après Soutenance Access content directly
Master Thesis Year : 2013

Generation of polynomial inequalities as invariants


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

Dates and versions

dumas-00854834 , version 1 (28-08-2013)


  • HAL Id : dumas-00854834 , version 1


Yannick Zakowski. Generation of polynomial inequalities as invariants. Symbolic Computation [cs.SC]. 2013. ⟨dumas-00854834⟩
272 View
494 Download


Gmail Facebook X LinkedIn More