Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Using Bounded Model Checking to Focus Fixpoint Iterations

  • Conference paper
Static Analysis (SAS 2011)

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

Included in the following conference series:

Abstract

Two classical sources of imprecision in static analysis by abstract interpretation are widening and merge operations. Merge operations can be done away by distinguishing paths, as in trace partitioning, at the expense of enumerating an exponential number of paths.

In this article, we describe how to avoid such systematic exploration by focusing on a single path at a time, designated by SMT-solving. Our method combines well with acceleration techniques, thus doing away with widenings as well in some cases. We illustrate it over the well-known domain of convex polyhedra.

This research was partially funded by ANR project “ASOPT”.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

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 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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Ancourt, C., Coelho, F., Irigoin, F.: A modular static analysis approach to affine loop invariants detection. Electr. Notes Theor. Comput. Sci. 267(1), 3–16 (2010); Proceedings of NSAD

    Article  MATH  Google Scholar 

  2. Armando, A., Mantovani, J., Platania, L.: Bounded model checking of software using smt solvers instead of sat solvers. International Journal on Software Tools for Technology Transfer (STTT) 11(1), 69–83 (2009)

    Article  MATH  Google Scholar 

  3. Bagnara, R., Hill, P.M., Zaffanella, E.: The Parma Polyhedra Library, version 0.9, http://www.cs.unipr.it/ppl

  4. Bagnara, R., Hill, P.M., Zaffanella, E.: Widening operators for powerset domains. International Journal on Software Tools for Technology Transfer (STTT) 8(4-5), 449–466 (2006); See also erratum in June 2007 issue

    Article  MATH  Google Scholar 

  5. Balakrishnan, G., Sankaranarayanan, S., Ivancic, F., Gupta, A.: Refining the control structure of loops using static analysis. In: Chakraborty, S., Halbwachs, N. (eds.) EMSOFT, pp. 49–58. ACM, New York (2009)

    Chapter  Google Scholar 

  6. Barrett, C., Ranise, S., Stump, A., Tinelli, C.: The satisfiability modulo theories library, SMT-LIB (2008), www.smtlib.org

  7. Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Path invariants. In: PLDI, pp. 300–309. ACM, New York (2007)

    Google Scholar 

  8. 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: Programming Language Design and Implementation (PLDI), pp. 196–207. ACM, New York (2003)

    Google Scholar 

  9. Bourdoncle, F.: Sémantique des langages impératifs d’ordre supérieur et interprétation abstraite. Ph.D. thesis, École polytechnique, Palaiseau (1992)

    Google Scholar 

  10. Bozga, M., Gîrlea, C., Iosif, R.: Iterating octagons. Tech. Rep. 16, VERIMAG (2008)

    Google Scholar 

  11. Bozga, M., Iosif, R., Konecny, F.: Fast acceleration of ultimately periodic relations. Tech. Rep. 2010-3, VERIMAG (2010)

    Google Scholar 

  12. Comon, H., Jurski, Y.: Multiple counters automata, safety analysis and Presburger arithmetic. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 268–279. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  13. Cousot, P.: Méthodes itératives de construction et d’approximation de points fixes d’opérateurs monotones sur un treillis, analyse sémantique des programmes. State doctorate thesis, Université scientifique et médicale de Grenoble and Institut National Polytechnique de Grenoble (1978), http://tel.archives-ouvertes.fr/tel-00288657/en/

  14. Cousot, P., Cousot, R.: Abstract interpretation frameworks. J. of Logic and Computation, 511–547 (August 1992)

    Google Scholar 

  15. Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: The ASTREÉ analyzer. In: Sagiv, S.M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 21–30. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  16. Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: Combination of abstractions in the ASTRÉE static analyzer. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol. 4435, pp. 272–300. Springer, Heidelberg (2008), http://www.di.ens.fr/~cousot/COUSOTpapers/ASIAN06.shtml

    Chapter  Google Scholar 

  17. Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Principles of Programming Languages (POPL), pp. 84–96. ACM, New York (1978)

    Google Scholar 

  18. Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: An efficient method of computing static single assignment form. In: Principles of Programming Languages (POPL), pp. 25–35. ACM, New York (1989)

    Google Scholar 

  19. Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81–94. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  20. Feautrier, P., Gonnord, L.: Accelerated invariant generation for C programs with Aspic and C2fsm. In: Tools (TAPAS) (2010)

    Google Scholar 

  21. Gawlitza, T.M., Monniaux, D.: Improving strategies via SMT solving. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 236–255. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  22. Gonnord, L.: Accelération abstraite pour l’amélioration de la précision en analyse des relations linéaires. Ph.D. thesis, Université Joseph Fourier (October 2007), http://tel.archives-ouvertes.fr/tel-00196899/en/

  23. Gonnord, L., Halbwachs, N.: Combining widening and acceleration in linear relation analysis. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 144–160. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  24. Gopan, D., Reps, T.W.: Lookahead widening. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 452–466. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  25. Gulwani, S., Srivastava, S., Venkatesan, R.: Constraint-based invariant inference over predicate abstraction. In: Jones, N.D., Müller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 120–135. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  26. Gulwani, S., Zuleger, F.: The reachability-bound problem. In: Zorn, B.G., Aiken, A. (eds.) PLDI, pp. 292–304. ACM, New York (2010)

    Google Scholar 

  27. Halbwachs, N.: Détermination automatique de relations linéaires vérifiées par les variables d’un programme. State doctorate thesis, Université scientifique et médicale de Grenoble and Institut National Polytechnique de Grenoble (1979), http://tel.archives-ouvertes.fr/tel-00288805/en/

  28. Halbwachs, N.: Delay analysis in synchronous programs. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 333–346. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  29. Kroening, D., Strichman, O.: Decision procedures. Springer, Heidelberg (2008)

    MATH  Google Scholar 

  30. Miné, A.: Symbolic methods to enhance the precision of numerical abstract domains. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 348–363. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  31. Monniaux, D.: Automatic modular abstractions for linear constraints. In: Pierce, B.C. (ed.) Symposium on Principles of Programming Languages (POPL). ACM, New York (2009)

    Google Scholar 

  32. Monniaux, D.: Automatic modular abstractions for template numerical constraints. Logical Methods in Computer Science (2010) (to appear)

    Google Scholar 

  33. Popeea, C., Chin, W.N.: Inferring disjunctive postconditions. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol. 4435, pp. 331–345. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  34. Reps, T.W., Sagiv, M., Yorsh, G.: Symbolic implementation of the best transformer. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 252–266. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  35. Rival, X.: Understanding the origin of alarms in astrée. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 303–319. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  36. Rival, X., Mauborgne, L.: The trace partitioning abstract domain. Transactions on Programming Languages and Systems (TOPLAS) 29(5), 26 (2007)

    Article  Google Scholar 

  37. Sankaranarayanan, S., Ivančić, F., Shlyakhter, I., Gupta, A.: Static analysis in disjunctive numerical domains. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 3–17. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CNRS, VERIMAG, Gières, France

    David Monniaux

  2. Université Lille 1, LIFL, Villeneuve d’Ascq, France

    Laure Gonnord

Authors
  1. David Monniaux
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Laure Gonnord
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computer Science Deptartement, Technion, 32000, Technion City, Haifa, Israel

    Eran Yahav

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Monniaux, D., Gonnord, L. (2011). Using Bounded Model Checking to Focus Fixpoint Iterations. In: Yahav, E. (eds) Static Analysis. SAS 2011. Lecture Notes in Computer Science, vol 6887. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-23702-7_27

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-23702-7_27

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-23701-0

  • Online ISBN: 978-3-642-23702-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation