Abstract
Abstract interpretation theory formalizes the idea of abstraction of mathematical structures, in particular those involved in the specification of properties and proof methods of computer systems. Verification by abstract interpretation is illustrated on the particular cases of predicate abstraction, which is revisited to handle infinitary abstractions, and on the new parametric predicate abstraction.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
T. Ball, R. Majumdar, T.D. Millstein and S.K. Rajamani. Automatic Predicate Abstraction of C Programs. In Proc. ACM SIGPLAN’ 2001 Conf. PLDI, pp. 203-213, 2001. ACM Press.
T. Ball, T. Millstein, and S. Rajamani. Polymorphic predicate abstraction. Tech. rep. MSR-TR-2001-10, Microsoft Research, Redmond, 17 June 2002. 21 p.
T. Ball, A. Podelski, and S. Rajamani. Relative completeness of abstraction refinement for software model checking. In J.-P. Katoen and P. Stevens, eds., Proc. 8 th Int. Conf. TACAS’ 2002, LNCS 2280, pp. 158-172. Springer, 2002.
N. Bjørner, I.A. Browne and Z. Manna. Automatic Generation of Invariants and Intermediate Assertions. Theor. Comp. Sci., 173(1):49–87, 199
B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and X. Rival. A static analyzer for large safety-critical software. In Proc. ACM SIGPLAN’ 2003 Conf. PLDI, pp. 196-207, 2003. ACM Press.
P. Černý. Vérification par intérprétation abstraite de prédicats paramétriques. D.E.A. report, Univ. Paris VII & École normale supérieure, Paris, 20 Sep. 2003.
P. Cousot. Méthodes itératives de construction et d’approximation de points fixes d’opérateurs monotones sur un treillis, analyse sémantique de programmes. Thèse d’État ès sciences mathématiques, Université scientifique et médicale de Grenoble, Grenoble, 21 Mar. 1978.
P. Cousot. Semantic foundations of program analysis. In S.S. Muchnick and N.D. Jones, editors, Program Flow Analysis: Theory and Applications, chapter 10, pages 303-342. Prentice-Hall, 1981.
P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In 4th POPL, pp. 238-252, 1977. ACM Press.
P. Cousot and R. Cousot. Automatic synthesis of optimal invariant assertions: mathematical foundations. In ACM Symp. on Artificial Intelligence & Programming Languages, ACM SIGPLAN Not. 12(8):1–12, 1977.
P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In 6th POPL, pp. 269-282, 1979. ACM Press.
P. Cousot and R. Cousot. Abstract interpretation and application to logic programs. J. Logic Programming 6, 13(2–3):103–179, 1992.
P. Cousot and R. Cousot. Abstract interpretation frameworks. J. Logic and Comp., 2(4):511–547, Aug. 1992.
P. Cousot and R. Cousot. Modular static program analysis, invited paper. In R. Horspool, ed., Proc. 11 th Int. Conf. CC’ 2002, pp. 159-178, 2002. LNCS 2304, Springer.
S. Graf and H. Saidi. Construction of abstract state graphs with PVS. In O. Grumberg, ed., Proc. 9th Int. Conf. CAV’ 97, LNCS 1254, pp. 72-83. Springer, 1997.
G. Kildall. A unified approach to global program optimization. In 1st POPL, pp. 194-206, 1973. ACMpress.
Z. Manna. Mathematical theory of computation. McGraw Hill, 1972.
A. Miné. A few graph-based relational numerical abstract domains. In M. Hermenegildo and G. Puebla, eds., SAS’02, LNCS 2477, pp. 117-132. Springer, 2002.
A. Mycroft. Completeness and predicate-based abstract interpretation. In Proc. PEPM’93, 1993, pp. 80-87. ACM Press, 1993.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Cousot, P. (2003). Verification by Abstract Interpretation. In: Dershowitz, N. (eds) Verification: Theory and Practice. Lecture Notes in Computer Science, vol 2772. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39910-0_11
Download citation
DOI: https://doi.org/10.1007/978-3-540-39910-0_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21002-3
Online ISBN: 978-3-540-39910-0
eBook Packages: Springer Book Archive