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.
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
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)
Blanchet, B., et al.: A static analyzer for large safety-critical software. In: PLDI (2003)
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
Brat, G., Venet, A.: Precise and scalable static program analysis of nasa flight software. In: IEEE Aerospace Conference (2005)
Cousot, P.: Asynchronous iterative methods for solving a fixed point system of monotone equations in a complete lattice. Technical Report 88, IMAG Lab (1977)
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)
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)
Cousot, P., Cousot, R.: Abstract interpretation and application to logic programs. J. Logic Prog. 2-3(13), 103–179 (1992)
Cousot, P., et al.: The ASTREÉ analyzer. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 21–30. Springer, Heidelberg (2005)
Feret, J.: Static analysis of digital filters. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 33–48. Springer, Heidelberg (2004)
Horwitz, S., Demers, A.J., Teitelbaum, T.: An efficient general iterative algorithm for dataflow analysis. Acta Informatica 24(6), 679–694 (1987)
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)
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)
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)
Miné, A.: The octagon abstract domain. In: AST 2001. IEEE, Los Alamitos (2001)
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)
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)
Miné, A.: Weakly Relational Numerical Abstract Domains. PhD thesis, École Polytechnique, Palaiseau, France (2004)
Venet, A., Brat, G.: Precise and efficient static array bound checking for large embedded C programs. In: PLDI (2004)
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
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)