Abstract
In this paper we study the relation between the lack of completeness in abstract interpretation of model-checking and the structure of the counterexamples produced by a model-checker. We consider two dual forms of completeness of an abstract interpretation: Forward and backward completeness. They correspond respectively to the standard γ/α completeness of an abstract interpretation and can be related with each other by adjunction. We give a constructive characterization of Clarke et al.’s spurious counterexamples in terms of both forward and backward completeness of the underlying abstract interpretation. This result allows us to understand the structure of the counterexamples that can be removed by systematically refining abstract domains to achieve completeness with respect to a given operation. We apply our result to improve static program analysis by refining the model-checking of an abstract interpretation.
This is a preview of subscription content, log in via an institution to check access.
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
E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent system using temporal logic specification. ACM Trans. Program. Lang. Syst., 8(2):244–263, 1986.
E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In Proc. of the 12th Internat. Conf. on Computer Aided Verification (CAV’ 00), volume 1855 of Lecture Notes in Computer Science, pages 154–169. Springer-Verlag, Berlin, 2000.
E. M. Clarke, O. Grumberg, and D. E. Long. Model checking and abstraction. ACM Trans. Program. Lang. Syst., 16(5):1512–1542, 1994.
P. Cousot. Types as abstract interpretations (Invited Paper). In Conference Record of the 24th ACM Symp. on Principles of Programming Languages (POPL’ 97), pages 316–331. ACM Press, New York, 1997.
P. Cousot. Partial completeness of abstract fixpoint checking, invited paper. In Proceedings of the Fourth International Symposium on Abstraction, Reformulations and Approximation, SARA’2000, Lecture Notes in Artificial Intelligence 1864, pages 1–25, Horseshoe Bay, Texas, USA, 26–29 July 2000. Springer-Verlag, Berlin, Germany.
P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the 4th ACM Symp. on Principles of Programming Languages (POPL’ 77), pages 238–252. ACM Press, New York, 1977.
P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Conference Record of the 6th ACM Symp. on Principles of Programming Languages (POPL’79), pages 269–282. ACM Press, New York, 1979.
P. Cousot and R. Cousot. Refining model checking by abstract interpretation. Automated Software Engineering, 6(1):69–95, 1999.
P. Cousot and R. Cousot. Temporal abstract interpretation. In Conference Record of the Twentyseventh Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 12–25, Boston, Mass., January 2000. ACM Press, New York,NY.
D. Dams, R. Gerth, and O. Grumberg. Abstract interpretation of reactive systems. ACM Trans. Program. Lang. Syst., 19(2):253–291, 1997.
E. A. Emerson. Temporal and modal logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics. Elsevier, Amsterdam and The MIT Press, Cambridge, Mass., 1990.
G. Filé, R. Giacobazzi, and F. Ranzato. A unifying view of abstract domain design. A CM Comput. Surv., 28(2):333–336, 1996.
R. Giacobazzi and F. Ranzato. Refining and compressing abstract domains. In P. Degano, R. Gorrieri, and A. Marchetti-Spaccamela, editors, Proc. of the 24th Internat. Colloq. on Automata, Languages and Programming (ICALP’ 97), volume 1256 of Lecture Notes in Computer Science, pages 771–781. Springer-Verlag, Berlin, 1997.
R. Giacobazzi, F. Ranzato, and F. Scozzari. Making abstract interpretation complete. Journal of the ACM, 47(2):361–416, March 2000.
C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and S. Bensalem. Property preserving abstractions for the verification of concurrent systems. Formal Methods Syst. Des., 6:1–36, 1995.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag, Berlin, 1992.
M. Müller-Olm, D. Schmidt, and B. Steffen. Model-checking. A tutorial introduction. In G. Filé, editor, Proceedings of the International Static Analysis Symposium (SAS’ 99), volume 1694 of Lecture Notes in Computer Science, pages 330–354. Springer-Verlag, Berlin, 1999.
A. Mycroft. Completeness and predicate-based abstract interpretation. In Proc. of the ACM Symp. on Partial Evaluation and Program Manipulation (PEPM’ 93), pages 179–185. ACM Press, New York, 1993.
F. Ranzato. On the completeness of model checking. In Proc. of European Symposium on Programming (ESOP’ 01), Lecture Notes in Computer Science. Springer-Verlag, Berlin, 2001.
D. A. Schmidt. Data flow analysis is model checking of abstract interpretation. In Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL’ 98), pages 38–48. ACM Press, New York, 1998.
D. A. Schmidt. Trace-based abstract interpretation of operational semantics. Lisp and Symbolic Computation, 10(3):237–271, 1998.
B. Steffen. Data flow analysis as model checking. In A. Meyer, editor, Proc. of Theoretical aspects of computer software (TACS’ 91), volume 526 of Lecture Notes in Computer Science, pages 346–364. Springer-Verlag, Berlin, 1991.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Giacobazzi, R., Quintarelli, E. (2001). Incompleteness, Counterexamples, and Refinements in Abstract Model-Checking. In: Cousot, P. (eds) Static Analysis. SAS 2001. Lecture Notes in Computer Science, vol 2126. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-47764-0_20
Download citation
DOI: https://doi.org/10.1007/3-540-47764-0_20
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42314-0
Online ISBN: 978-3-540-47764-8
eBook Packages: Springer Book Archive