Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Automated Technology for Verification and Analysis

ATVA 2016: Automated Technology for Verification and Analysis pp 479–494Cite as

Polynomial Invariants by Linear Algebra

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9938))

Abstract

We present in this paper a new technique for generating polynomial invariants, divided in two independent parts: a procedure that reduces polynomial assignments composed loops analysis to linear loops under certain hypotheses and a procedure for generating inductive invariants for linear loops. Both of these techniques have a polynomial complexity for a bounded number of variables and we guarantee the completeness of the technique for a bounded degree which we successfully implemented for C programs verification.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

References

  1. Alur, R., Etessami, K., Madhusudan, P.: A temporal logic of nested calls and returns. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 467–481. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  2. Basu, S.K., Misra, J.: Proving loop programs. IEEE Trans. Softw. Eng. 1(1), 76–86 (1975)

    Article  MathSciNet  Google Scholar 

  3. Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Path invariants. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 300–309 (2007)

    Google Scholar 

  4. Botella, B., Delahaye, M., Ha, S.H.T., Kosmatov, N., Mouy, P., Roger, M., Williams, N.: Automating structural testing of C programs: experience with PathCrawler. In: 4th International Workshop on Automation of Software Test, AST, pp. 70–78 (2009)

    Google Scholar 

  5. Cachera, D., Jensen, T.P., Jobin, A., Kirchner, F.: Inference of polynomial invariants for imperative programs: a farewell to Gröbner bases. Sci. Comput. Program. 93, 89–109 (2014)

    Article  Google Scholar 

  6. Carbonell, E.: Polynomial invariant generation. http://www.cs.upc.edu/erodri/webpage/polynomial_invariants/list.html

  7. Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. CAV 2000, 154–169 (2000)

    MATH  Google Scholar 

  8. Cooper, K.D., Simpson, L.T., Vick, C.A.: Operator strength reduction. ACM Trans. Program. Lang. Syst. 23(5), 603–625 (2001)

    Article  Google Scholar 

  9. de Oliveira, S., Bensalem, S., Prevosto, V.: Polynomial invariants by linear algebra. Technical report 16–0065/SDO, CEA (2016). http://steven-de-oliveira.perso.sfr.fr/content/publis/pilat_tech_report.pdf

  10. Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)

    Article  MATH  Google Scholar 

  11. Hoare, C.A.R.: The verifying compiler: a grand challenge for computing research. J. ACM 50(1), 63–69 (2003)

    Article  MATH  Google Scholar 

  12. Hojjat, H., Iosif, R., Konečný, F., Kuncak, V., Rümmer, P.: Accelerating interpolants. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 187–202. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  13. Johnson, D.B.: Finding all the elementary circuits of a directed graph. SIAM J. Comput. 4(1), 77–84 (1975)

    Article  MathSciNet  MATH  Google Scholar 

  14. Kauers, M., Zimmermann, B.: Computing the algebraic relations of C-finite sequences and multisequences. J. Symb. Comput. 43(11), 787–803 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  15. Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. Formal Aspects Comput. 27(3), 573–609 (2015)

    Article  MathSciNet  Google Scholar 

  16. Kovács, L.: Aligator: a mathematica package for invariant generation (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 275–282. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  17. Kovács, L.: A complete invariant generation approach for P-solvable loops. In: Pnueli, A., Virbitskaite, I., Voronkov, A. (eds.) PSI 2009. LNCS, vol. 5947, pp. 242–256. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  18. Mayr, E.: Membership in polynomial ideals over Q is exponential space complete. In: Monien, B., Cori, R. (eds.) STACS 1989. LNCS, vol. 349, pp. 400–406. Springer, Heidelberg (1989)

    Google Scholar 

  19. Müller-Olm, M., Seidl, H.: Polynomial constants are decidable. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 4–19. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  20. Müller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra. POPL 2004, 330–341 (2004)

    MATH  Google Scholar 

  21. Pan, V.Y., Chen, Z.Q.: The complexity of the matrix eigenproblem. In: Proceedings of the Thirty-First Annual ACM Symposium on Theory of Computing, May 1–4, Atlanta, Georgia, USA, pp. 507–516 (1999)

    Google Scholar 

  22. Rodríguez-Carbonell, E., Kapur, D.: Generating all polynomial invariants in simple loops. J. Symbolic Comput. 42(4), 443–476 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  23. Tarjan, R.E.: Depth-first search and linear graph algorithms. SIAM J. Comput. 1(2), 146–160 (1972)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CEA, LIST, Software Reliability and Security Lab, CEA Saclay - Nano Innov - Bât 862 - PC 174, 91191, Gif Sur Yvette Cedex, France

    Steven de Oliveira & Virgile Prevosto

  2. Université Grenoble Alpes, Saint-martin-d’hàres, France

    Saddek Bensalem

Authors
  1. Steven de Oliveira
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Saddek Bensalem
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Virgile Prevosto
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Steven de Oliveira .

Editor information

Editors and Affiliations

  1. AIST , Osaka, Japan

    Cyrille Artho

  2. Inria Rennes , Rennes, France

    Axel Legay

  3. Bar Ilan University , Ramat Gan, Israel

    Doron Peled

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

de Oliveira, S., Bensalem, S., Prevosto, V. (2016). Polynomial Invariants by Linear Algebra. In: Artho, C., Legay, A., Peled, D. (eds) Automated Technology for Verification and Analysis. ATVA 2016. Lecture Notes in Computer Science(), vol 9938. Springer, Cham. https://doi.org/10.1007/978-3-319-46520-3_30

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-46520-3_30

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-46519-7

  • Online ISBN: 978-3-319-46520-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation