More Web Proxy on the site http://driver.im/

Article

Combination of abstractions in the ASTRÉE static analyzer

Authors:

Patrick Cousot,

Jérôme Feret,

Laurent Mauborgne,

David Monniaux,

Xavier RivalAuthors Info & Claims

ASIAN'06: Proceedings of the 11th Asian computing science conference on Advances in computer science: secure software and related issues

Pages 272 - 300

Published: 06 December 2006 Publication History

Abstract

We describe the structure of the abstract domains in the ASTRÉE static analyzer, their modular organization into a hierarchical network, their cooperation to over-approximate the conjunction/reduced product of different abstractions and to ensure termination using collaborative widenings and narrowings. This separation of the abstraction into a combination of cooperative abstract domains makes ASTRÉE extensible, an essential feature to cope with false alarms and ultimately provide sound formal verification of the absence of runtime errors in very large software.

References

[1]

Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: 4^th ACM POPL, pp. 238-252 (1977)

Digital Library

[2]

Cousot, P., Cousot, R.: Abstract interpretation frameworks. Journal of Logic and Computation 2, 511-547 (1992)

[3]

Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software, invited chapter. In: Mogensen, T., Schmidt, D., Sudborough, I. (eds.) The Essence of Computation. LNCS, vol. 2566, pp. 85-108. Springer, Heidelberg (2002)

Digital Library

[4]

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. ACM SIGPLAN'2003 Conf, PLDI, San Diego, pp. 196-207. ACMPress, New York (2003)

Digital Library

[5]

Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: The ASTRÉE analyzer. In: Sagiv, M. (ed.) Proc. 14th ESOP'2005, Edinburgh, 4-8 Apr. 2005. LNCS 3444, pp. 21-30. Springer, Heidelberg (2005)

Digital Library

[6]

Mauborgne, L.: ASTRÉE: Verification of absence of run-time error. In: Jacquart, P. (ed.) Building the Information Society, pp. 385-392. Kluwer Academic Publishers, Dordrecht (2004)

[7]

Miné, A.: Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics. In: Proc. LCTES 2006. Ottawa, Ontario, Canada, 14-16 June 2006, pp. 54-63. ACM Press, New York (2006)

Digital Library

[8]

Monniaux, D.: The parallel implementation of the ASTRÉE static analyzer. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, Springer, Heidelberg (2005)

Digital Library

[9]

Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Proceedings of the Second International Symposium on Programming, Paris, France, Dunod, Paris, France, pp. 106-130 (1976)

[10]

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)

Digital Library

[11]

Miné, A.: The octagon abstract domain. Higher-Order and Symbolic Computation 19, 31-100 (2006)

Digital Library

[12]

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

[13]

Feret, J.: The arithmetic-geometric progression abstract domain. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 2-58. Springer, Heidelberg (2005)

Digital Library

[14]

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

Digital Library

[15]

Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: 6th ACM POPL, pp. 269-282 (1979)

Digital Library

[16]

Leroy, X., Doligez, D., Garrigue, J., Rémy, D., Vouillon, J.: The Objective Caml system, documentation and user's manual (release 3.06). Technical report, INRIA, Rocquencourt, France (2002)

[17]

Miné, A.: The octagon abstract domain library (2006), www.di.ens.fr/~mine/oct/

[18]

ANSI/ISO: Programming languages - C. (1999) Standard ISO/IEC 9899:1999(E)

[19]

Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with BLAST. In: Ball, T., Rajamani, S.K. (eds.) Model Checking Software. LNCS, vol. 2648, pp. 235-239. Springer, Heidelberg (2003)

Digital Library

[20]

Cousot, P.: Verification by abstract interpretation, invited chapter. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 243-268. Springer, Heidelberg (2004)

[21]

Cousot, P.: The calculational design of a generic abstract interpreter, invited chapter. In: Broy, M., Steinbrüggen, R. (eds.) Calculational System Design. NATO Science Series, Series F: Computer and Systems Sciences, vol. 173, pp. 421-505. IOS Press, Amsterdam (1999)

[22]

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)

[23]

Cousot, P.: MIT course 16.399: Abstract Interpretation (2005), http://web.mit. edu/afs/athena.mit.edu/course/16/16.399/www/

Cited By

Toman JGrossman D(2019)Concerto: a framework for combined concrete and abstract interpretationProceedings of the ACM on Programming Languages10.1145/32903563:POPL(1-29)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290356
Hübner FHuang WPeleska J(2019)Experimental evaluation of a novel equivalence class partition testing strategySoftware and Systems Modeling (SoSyM)10.1007/s10270-017-0595-818:1(423-443)Online publication date: 1-Feb-2019
https://dl.acm.org/doi/10.1007/s10270-017-0595-8
Keidel SPoulsen CErdweg S(2018)Compositional soundness proofs of abstract interpretersProceedings of the ACM on Programming Languages10.1145/32367672:ICFP(1-26)Online publication date: 30-Jul-2018
https://dl.acm.org/doi/10.1145/3236767
Show More Cited By

Combination of abstractions in the ASTRÉE static analyzer
1. Theory of computation
  1. Logic
  2. Semantics and reasoning
    1. Program reasoning

Recommendations

Astrée: from research to industry
SAS'07: Proceedings of the 14th international conference on Static Analysis

Airbus has started introducing abstract interpretation based static analysers into the verification process of some of its avionics software products. Industrial constraints require any such tool to be extremely precise, which can only be achieved after ...
The parallel implementation of the astrée static analyzer
APLAS'05: Proceedings of the Third Asian conference on Programming Languages and Systems

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 ...
Why does Astrée scale up?

Astrée was the first static analyzer able to prove automatically the total absence of runtime errors of actual industrial programs of hundreds of thousand lines. What makes Astrée such an innovative tool is its scalability, while retaining ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

ASIAN'06: Proceedings of the 11th Asian computing science conference on Advances in computer science: secure software and related issues

December 2006

361 pages

ISBN:3540775048

Editors:
Mitsu Okada
Keio University, Japan
,
Ichiro Satoh
National Institute of Informatics, Japan

Sponsors

Keio University: Keio University
The National Institute of Informatics
The Embassy of France in Japan
INRIA: Institut Natl de Recherche en Info et en Automatique

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 06 December 2006

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

28
Total Citations
View Citations
1
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 15 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Toman JGrossman D(2019)Concerto: a framework for combined concrete and abstract interpretationProceedings of the ACM on Programming Languages10.1145/32903563:POPL(1-29)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290356
Hübner FHuang WPeleska J(2019)Experimental evaluation of a novel equivalence class partition testing strategySoftware and Systems Modeling (SoSyM)10.1007/s10270-017-0595-818:1(423-443)Online publication date: 1-Feb-2019
https://dl.acm.org/doi/10.1007/s10270-017-0595-8
Keidel SPoulsen CErdweg S(2018)Compositional soundness proofs of abstract interpretersProceedings of the ACM on Programming Languages10.1145/32367672:ICFP(1-26)Online publication date: 30-Jul-2018
https://dl.acm.org/doi/10.1145/3236767
Beyer DJakobs MLemberger TWehrheim HChaudron MCrnkovic IChechik MHarman M(2018)Reducer-based construction of conditional verifiersProceedings of the 40th International Conference on Software Engineering10.1145/3180155.3180259(1182-1193)Online publication date: 27-May-2018
https://dl.acm.org/doi/10.1145/3180155.3180259
Jourdan JLaporte VBlazy SLeroy XPichardie D(2015)A Formally-Verified C Static AnalyzerACM SIGPLAN Notices10.1145/2775051.267696650:1(247-259)Online publication date: 14-Jan-2015
https://dl.acm.org/doi/10.1145/2775051.2676966
Jourdan JLaporte VBlazy SLeroy XPichardie DRajamani SWalker D(2015)A Formally-Verified C Static AnalyzerProceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages10.1145/2676726.2676966(247-259)Online publication date: 14-Jan-2015
https://dl.acm.org/doi/10.1145/2676726.2676966
Cousot PCousot RHenzinger TMiller D(2014)Abstract interpretationProceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1145/2603088.2603165(1-10)Online publication date: 14-Jul-2014
https://dl.acm.org/doi/10.1145/2603088.2603165
Apinis KSeidl HVojdani V(2013)How to combine widening and narrowing for non-monotonic systems of equationsACM SIGPLAN Notices10.1145/2499370.246219048:6(377-386)Online publication date: 16-Jun-2013
https://dl.acm.org/doi/10.1145/2499370.2462190
Apinis KSeidl HVojdani VBoehm HFlanagan C(2013)How to combine widening and narrowing for non-monotonic systems of equationsProceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/2491956.2462190(377-386)Online publication date: 16-Jun-2013
https://dl.acm.org/doi/10.1145/2491956.2462190
Cousot PCousot RMauborgne L(2013)Theories, solvers and static analysis by abstract interpretationJournal of the ACM10.1145/2395116.239512059:6(1-56)Online publication date: 9-Jan-2013
https://dl.acm.org/doi/10.1145/2395116.2395120
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Table of Contents