Skip to Main content Skip to Navigation
Master Thesis

Generation of polynomial inequalities as invariants

Abstract : 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.
Complete list of metadata

Cited literature [46 references]  Display  Hide  Download

https://dumas.ccsd.cnrs.fr/dumas-00854834
Contributor : Co-Responsables Du Mri V. Gouranton Et S. Blazy Connect in order to contact the contributor
Submitted on : Wednesday, August 28, 2013 - 11:25:59 AM
Last modification on : Tuesday, October 19, 2021 - 11:58:53 PM
Long-term archiving on: : Monday, December 2, 2013 - 8:49:15 AM

Identifiers

  • HAL Id : dumas-00854834, version 1

Citation

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

Share

Metrics

Record views

257

Files downloads

472