Abstract
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 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.
This work has been partially supported by PRIN project “AIDA — Abstract Interpretation: Design and Applications,” by the “LogicTools” project (CICYT TIN 2004-03382), and the FPU grant AP2002-3693 from the Spanish MEC.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Bagnara, R.: Data-Flow Analysis for Constraint Logic-Based Languages. PhD thesis, Dipartimento di Informatica, Università di Pisa, Pisa, Italy (March 1997)
Bagnara, R., Hill, P.M., Ricci, E., Zaffanella, E.: Precise widening operators for convex polyhedra. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 337–354. Springer, Heidelberg (2003)
Bagnara, R., Hill, P.M., Ricci, E., Zaffanella, E.: Precise widening operators for convex polyhedra. Science of Computer Programming (2005) (to appear)
Bagnara, R., Ricci, E., Zaffanella, E., Hill, P.M.: Possibly not closed convex polyhedra and the parma polyhedra library. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 213–229. Springer, Heidelberg (2002)
Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: FAST: Fast acceleration of symbolic transition systems. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 118–121. Springer, Heidelberg (2003)
Bensalem, S., Bozga, M., Fernández, J.-C., Ghirvu, L., Lakhnech, Y.: A transformational approach for generating non-linear invariants. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol. 1824, pp. 58–74. Springer, Heidelberg (2000)
Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: Proc. PLDI 2003, San Diego, CA, pp. 196–207 (2003)
Colón, M.: Approximating the algebraic relational semantics of imperative programs. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 296–311. Springer, Heidelberg (2004)
Cousot, P.: Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 1–24. Springer, Heidelberg (2005)
Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Proc. ISOP 1976, Paris, France, pp. 106–130 (1976)
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. POPL 1977, New York, pp. 238–252 (1977)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proc. POPL 1979, New York, pp. 269–282 (1979)
Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: The ASTRÉE analyzer. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 21–30. Springer, Heidelberg (2005)
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proc. POPL 1978, Tucson, AR, pp. 84–96 (1978)
Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)
Freire, P.: SQRT (2002), http://www.pedrofreire.com/sqrt , Retrieved April 10, 2005
Halbwachs, N.: Delay analysis in synchronous programs. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 333–346. Springer, Heidelberg (1993)
Hsieh, P.: How to calculate square roots (2004), http://www.azillionmonkeys.com/qed/sqroot.html , Retrieved April 10, 2005
Kapur, D.: Automatically generating loop invariants using quantifier elimination. In: Proc. ACA 2004, Beaumont, Texas (2004)
Karr, M.: Affine relationships among variables of a program. Acta Informatica. 6, 133–151 (1976)
Mastroeni, I.: Algebraic power analysis by abstract interpretation. Higher-Order and Symbolic Computation 17(4), 297–345 (2004)
Miné, A.: The octagon abstract domain. In: Proc. WCRE 2001, Stuttgart, Germany, pp. 310–319 (2001)
Müller-Olm, M., Seidl, H.: Computing polynomial program invariants. Information Processing Letters 91(5), 233–244 (2004)
Müller-Olm, M., Seidl, H.: A note on karr’s algorithm. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 1016–1028. Springer, Heidelberg (2004)
Müller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra. In: Proc. POPL 2004, Venice, Italy, pp. 330–341 (2004)
Rodríguez-Carbonell, E., Kapur, D.: An abstract interpretation approach for automatic generation of polynomial invariants. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 280–295. Springer, Heidelberg (2004)
Rodríguez-Carbonell, E., Kapur, D.: Automatic generation of polynomial loop invariants: Algebraic foundations. In: Proc. ISSAC 2004, Santander, pp. 266–273 (2004)
Roozbehani, M., Feron, E., Megrestki, A.: Modeling, optimization and computation for software verification. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 606–622. Springer, Heidelberg (2005)
Sankaranarayanan, S., Sipma, H., Manna, Z.: Constraint-based linear-relations analysis. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 53–68. Springer, Heidelberg (2004)
Sankaranarayanan, S., Sipma, H., Manna, Z.: Scalable analysis of linear systems using mathematical programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 25–41. Springer, Heidelberg (2005)
Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Non-linear loop invariant generation using Gröbner bases. In: Proc. POPL 2004, Venice, Italy, pp. 318–329 (2004)
Simmons, R.: Commonsense arithmetic reasoning. In: Proc. AAAI 1986, Philadelphia, PA, vol. 1, pp. 118–124 (1986)
Stoer, J., Witzgall, C.: Convexity and Optimization in Finite Dimensions I. Springer, Berlin (1970)
Tiwari, A., Rueß, H., Saïdi, H., Shankar, N.: A technique for invariant generation. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 113–127. Springer, Heidelberg (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bagnara, R., Rodríguez-Carbonell, E., Zaffanella, E. (2005). Generation of Basic Semi-algebraic Invariants Using Convex Polyhedra. In: Hankin, C., Siveroni, I. (eds) Static Analysis. SAS 2005. Lecture Notes in Computer Science, vol 3672. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11547662_4
Download citation
DOI: https://doi.org/10.1007/11547662_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-28584-7
Online ISBN: 978-3-540-31971-9
eBook Packages: Computer ScienceComputer Science (R0)