Skip to main content
SpringerLink
Log in

The Parallel Implementation of the Astrée Static Analyzer

  • Conference paper
Programming Languages and Systems (APLAS 2005)

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

Included in the following conference series:

Abstract

The Astrée static analyzer is a specialized tool that can prove the absence of runtime errors, including arithmetic overflows, in large critical programs. Keeping analysis times reasonable for industrial use is one of the design objectives. In this paper, we discuss the parallel implementation of the analysis.

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

Access this chapter

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

References

  1. Blanchet, B., et al.: Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In: Mogensen, T.Æ., Schmidt, D.A., Sudborough, I.H. (eds.) The Essence of Computation. LNCS, vol. 2566, pp. 85–108. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  2. Blanchet, B., et al.: A static analyzer for large safety-critical software. In: PLDI (2003)

    Google Scholar 

  3. Bourdoncle, F.: Efficient chaotic iteration strategies with widenings. In: Pottosin, I.V., Bjorner, D., Broy, M. (eds.) FMP&TA 1993. LNCS, vol. 735, p. 128. Springer, Heidelberg (1993), http://citeseer.ist.psu.edu/article/bourdoncle93efficient.html

    Chapter  Google Scholar 

  4. Brat, G., Venet, A.: Precise and scalable static program analysis of nasa flight software. In: IEEE Aerospace Conference (2005)

    Google Scholar 

  5. Cousot, P.: Asynchronous iterative methods for solving a fixed point system of monotone equations in a complete lattice. Technical Report 88, IMAG Lab (1977)

    Google Scholar 

  6. Cousot, P.: The calculational design of a generic abstract interpreter. In: Broy, M., Steinbrüggen, R. (eds.) Calculational System Design. NATO ASI Series F. IOS Press, Amsterdam (1999)

    Google Scholar 

  7. Cousot, P., Cousot, R.: Abstract intrepretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, Los Angeles, CA, January 1977, pp. 238–252 (1977)

    Google Scholar 

  8. Cousot, P., Cousot, R.: Abstract interpretation and application to logic programs. J. Logic Prog. 2-3(13), 103–179 (1992)

    Article  MathSciNet  Google Scholar 

  9. Cousot, P., et al.: The ASTREÉ analyzer. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 21–30. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  10. Feret, J.: Static analysis of digital filters. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 33–48. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  11. Horwitz, S., Demers, A.J., Teitelbaum, T.: An efficient general iterative algorithm for dataflow analysis. Acta Informatica 24(6), 679–694 (1987)

    Article  MATH  MathSciNet  Google Scholar 

  12. Mauborgne, L., Rival, X.: Trace partitioning in abstract interpretation based static analyzers. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 5–20. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  13. Mertens, S.: The easiest hard problem: Number partitioning. In: Percus, A.G., Istrate, G., Moore, C. (eds.) Computational Complexity and Statistical Physics, p. 8. Oxford University Press, Oxford (2004)

    Google Scholar 

  14. Miné, A.: A new numerical abstract domain based on difference-bound matrices. In: Danvy, O., Filinski, A. (eds.) PADO 2001. LNCS, vol. 2053, p. 155. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  15. Miné, A.: The octagon abstract domain. In: AST 2001. IEEE, Los Alamitos (2001)

    Google Scholar 

  16. Miné, A.: A few graph-based relational numerical abstract domains. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, p. 117. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  17. Miné, A.: Relational abstract domains for the detection of floating-point run-time errors. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 3–17. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  18. Miné, A.: Weakly Relational Numerical Abstract Domains. PhD thesis, École Polytechnique, Palaiseau, France (2004)

    Google Scholar 

  19. Venet, A., Brat, G.: Precise and efficient static array bound checking for large embedded C programs. In: PLDI (2004)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Centre national de la recherche scientifique (CNRS), École normale supérieure, Laboratoire d’Informatique, 45 rue d’Ulm, 75230 cedex 5, Paris, France

    David Monniaux

Authors
  1. David Monniaux
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Seoul National University, Korea

    Kwangkeun Yi

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Monniaux, D. (2005). The Parallel Implementation of the Astrée Static Analyzer. In: Yi, K. (eds) Programming Languages and Systems. APLAS 2005. Lecture Notes in Computer Science, vol 3780. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11575467_7

Download citation

  • DOI: https://doi.org/10.1007/11575467_7

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-29735-2

  • Online ISBN: 978-3-540-32247-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation