Abstract
Abstract Interpretation is a theory of approximation of mathematical structures, in particular those involved in the semantic models of computer systems [4,10,11]. Abstract interpretation can be applied to the systematic construction of methods and effective algorithms to approximate undecidable or very complex problems in computer science. The scope of application is rather large e.g. from type inference [5], model-checking [13], program transformation [14], watermarking [15] to context-free grammar parser generation [16].
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., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: The Astrée Static Analyzer, http://www.astree.ens.fr/
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. 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., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: Proceedings of the ACM SIGPLAN ’2003 Conference on Programming Language Design and Implementation (PLDI), San Diego, California, United States, June 7-14, 2003, pp. 196–207. ACM Press, New York (2003)
Cousot, P.: Méthodes itératives de construction et d’approximation de points fixes d’opérateurs monotones sur un treillis, analyse sémantique de programmes (in French). In: Thèse d’État ès sciences mathématiques, Université scientifique et médicale de Grenoble, Grenoble, France, March 21, (1978)
Cousot, P.: Types as abstract interpretations. In: Conference Record of the Twentyfourth Annual ACM SIGPLAN--SIGACT Symposium on Principles of Programming Languages, Paris, France, January 1997, pp. 316–331. ACM Press, New York (1997)
Cousot, P.: Partial completeness of abstract fixpoint checking. In: Choueiry, B.Y., Walsh, T. (eds.) SARA 2000. LNCS (LNAI), vol. 1864, pp. 1–25. Springer, Heidelberg (2000)
Cousot, P.: Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Theoretical Computer Science 277(1—2), 47–103 (2002)
Cousot, P.: Integrating physical systems in the static analysis of embedded control software. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 135–138. Springer, Heidelberg (2005)
Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Proceedings of the Second International Symposium on Programming, Paris, France, pp. 106–130. Dunod, Paris, France (1976)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the Fourth Annual ACM SIGPLAN--SIGACT Symposium on Principles of Programming Languages, Los Angeles, California. United States, pp. 238–252. ACM Press, New York (1977)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Conference Record of the Sixth Annual ACM SIGPLAN--SIGACT Symposium on Principles of Programming Languages, San Antonio, Texas, pp. 269–282. ACM Press, New York (1979)
Cousot, P., Cousot, R.: Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. In: Bruynooghe, M., Wirsing, M. (eds.) PLILP 1992. LNCS, vol. 631, pp. 269–295. Springer, Heidelberg (1992)
Cousot, P., Cousot, R.: Temporal abstract interpretation. In: Conference Record of the Twentyseventh Annual ACM SIGPLAN--SIGACT Symposium on Principles of Programming Languages, Boston, Massachusetts, United States, January 2000, pp. 12–25. ACM Press, New York (2000)
Cousot, P., Cousot, R.: Systematic design of program transformation frameworks by abstract interrpetation. In: Conference Record of the Twentyninth Annual ACM SIGPLAN--SIGACT Symposium on Principles of Programming Languages, Portland, Oregon, United States, January 2002, pp. 178–190. ACM Press, New York (2002)
Cousot, P., Cousot, R.: An abstract interpretation-based framework for software watermarking. In: Conference Record of the Thirtyfirst Annual ACM SIGPLAN--SIGACT Symposium on Principles of Programming Languages, Venice, Italy, January 14–16, 2004, pp. 173–185. ACM Press, New York (2004)
Cousot, P., Cousot, R.: Grammar analysis and parsing by abstract interpretation. In: Reps, T., Sagiv, M., Bauer, J. (eds.) Program Analysis and Compilation, Theory and Practice. LNCS, vol. 4444, pp. 175–200. Springer, Heidelberg (2007)
Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: The Astrée analyser. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 21–30. Springer, Heidelberg (2005)
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.) Eleventh Annual Asian Computing Science Conference, ASIAN 06, LNCS, Tokyo, Japan, December 6–8, 2006. pp. 6–8. Springer, Berlin (to appear, 2006)
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Conference Record of the Fifth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Tucson, Arizona, pp. 84–97. ACM Press, New York (1978)
Feret, J.: Static analysis of digital filters. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 33–48. Springer, Heidelberg (2004)
Feret, J.: The arithmetic-geometric progression abstract domain. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 42–58. Springer, Heidelberg (2005)
Hoare, C.A.R.: The verifying compiler, a grand challenge for computing research. Journal of the Association for Computing Machinary 50(1), 63–69 (2003)
Hoare, C.A.R.: The verifying compiler, a grand challenge for computing research. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, p. 78. Springer, Heidelberg (2005)
Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: Conference Record of the Thirtythird Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Charleston, South Carolina, pp. 42–54. ACM Press, New York (2006)
Mauborgne, L.: Astrée: Verification of absence of run-time error. In: Jacquart, P. (ed.) Building the Information Society, ch. 4, pp. 385–392. Kluwer Academic Publishers, Dordrecht (2004)
Mauborgne, L., Rival, X.: Trace partitioning in abstract interpretation based static analyzer. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 5–20. Springer, Heidelberg (2005)
Miné, A.: The Octagon abstract domain library. http://www.di.ens.fr/~mine/oct/
Miné, A.: A new numerical abstract domain based on difference-bound matrices. In: Danvy, O., Filinski, A. (eds.) PADO 2001. LNCS, vol. 2053, pp. 155–172. Springer, Heidelberg (2001)
Miné, A.: A few graph-based relational numerical abstract domains. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 117–132. 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.: Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics. In: Proceedings of the ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems, LCTES ’2006, June 2006, pp. 54–63. ACM Press, New York (2006)
Miné, A.: The octagon abstract domain. Higher-Order and Symbolic Computation 19, 31–100 (2006)
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)
Monniaux, D.: The parallel implementation of the Astrée static analyzer. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 86–96. Springer, Heidelberg (2005)
Rival, X.: Abstract interpretation based certification of assembly code. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 41–55. Springer, Heidelberg (2002)
Rival, X.: Invariant translation-based certification of assembly code. International Journal on Software and Tools for Technology Transfer 6(1), 15–37 (2004)
Rival, X.: Symbolic transfer functions-based approaches to certified compilation. In: Conference Record of the Thirtyfirst Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Venice, Italy, pp. 1–13. ACM Press, New York (2004)
Rival, X.: Abstract dependences for alarm diagnosis. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 347–363. Springer, Heidelberg (2005)
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)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Cousot, P. (2008). The Verification Grand Challenge and Abstract Interpretation. In: Meyer, B., Woodcock, J. (eds) Verified Software: Theories, Tools, Experiments. VSTTE 2005. Lecture Notes in Computer Science, vol 4171. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69149-5_21
Download citation
DOI: https://doi.org/10.1007/978-3-540-69149-5_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69147-1
Online ISBN: 978-3-540-69149-5
eBook Packages: Computer ScienceComputer Science (R0)