@Inproceedings{BagnaraR-CZ05,
  Author = "R. Bagnara and E. Rodr{\'\i}guez-Carbonell and E. Zaffanella",
  Title = "Generation of Basic Semi-algebraic Invariants
           Using Convex Polyhedra",
  Booktitle = "Static Analysis:
               Proceedings of the 12th International Symposium",
  Address = "London, UK",
  Editor = "C. Hankin and I. Siveroni",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 3672,
  ISBN = "3-540-28584-9",
  Year = 2005,
  Pages = "19--34",
  Abstract = "A technique for generating invariant polynomial
              \emph{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."
}