Generation of Basic Semi-algebraic Invariants Using Convex Polyhedra

Publication TypeConference Paper
Year of Publication2005
AuthorsBagnara R, Rodríguez-Carbonell E, Zaffanella E
EditorHankin C, Siveroni I
Conference NameStatic Analysis: Proceedings of the 12th International Symposium
PublisherSpringer-Verlag, Berlin
Conference LocationLondon, UK
ISBN Number3-540-28584-9
Keywordsabstract interpretation, nonlinear invariants, numerical properties, software verification, static analysis

A technique for generating invariant polynomial inequalities of bounded degree is presented using the abstract interpretation framework. It is based on overapproximating basic semi-algebraic sets, i.e., sets defined by conjunctions of polynomial inequalities, by means of convex polyhedra. While improving on the existing methods for generating invariant polynomial \emph{equalities}, since polynomial inequalities are allowed in the guards of the transition system, the approach does not suffer from the prohibitive complexity of the methods based on quantifier-elimination. The application of our implementation to benchmark programs shows that the method produces non-trivial invariants in reasonable time. In some cases the generated invariants are essential to verify safety properties that cannot be proved with classical linear invariants.

File attachments: 
We are a passionate team of experts. Do not hesitate to let us have your feedback:
You may be surprised to discover just how much your suggestions matter to us.