Abstract.
We present a new, on-the-fly algorithm that given a push-down model representing a sequential program with (recursive) procedure calls and an extended finite-state automaton representing (the negation of) a safety property, produces a succinct, symbolic representation of all counter-examples; i.e., traces of system behaviors that violate the property. The class of what we call minimum-recursion loop-free counter-examples can then be generated from this representation on an as-needed basis and presented to the user. Our algorithm is also applicable, without modification, to finite-state system models. Simultaneous consideration of multiple counter-examples can minimize the number of model-checking runs needed to recognize common root causes of property violations. We illustrate the use of our techniques via application to a Java-Tar utility and an FTP-server program, and discuss a prototype tool implementation which offers several abstraction techniques for easy-viewing of generated counter-examples.
Research supported in part by ONR grant N000140110967, NSF grants CCR-0205376 and CCR-9988155, and ARO grants DAAD190110003 and DAAD190110019.
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
Alur, R., Dang, T., Ivančić, F.: Counter-example guided predicate abstraction of hybrid systems. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems (2003)
Ball, T., Naik, M., Rajamani, S.K.: From symptom to cause: Localizing errors in counterexample traces. In: Symposium on Principles of Programming Languages (2003)
Basu, S., Kumar, K.N., Pokorny, R.L., Ramakrishnan, C.R.: Resource-constrained model checking for recursive programs. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems (2002)
Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model checking. Concurrency Theory (1997)
Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems 8(2) (1986)
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: 12th International Conference Computer Aided Verification (2000)
Das, S., Dill, D.L.: Counter-example based predicate discovery in predicate abstraction. In: 4th International Conference on Formal Methods in Computer-Aided Design (2002)
Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient algorithms for model checking pushdown systems. In: 12th International Conference Computer Aided Verification, pp. 232–247. Springer, Heidelberg (2000)
Esparza, J., Schwoon, S.: A BDD-based model checker for recursive programs. In: 13th International Conference Computer Aided Verification, pp. 324–336. Springer, Heidelberg (2001)
Finkel, A., Willems, B., Wolper, P.: A direct symbolic approach to model checking pushdown systems. In: 2nd International Workshop on Verification of Infinite State System, vol. 9. Elsevier Science, Amsterdam (1997)
Glusman, M., Kamhi, G., Mador-Haim, S., Fraer, R., Vardi, M.Y.: Multiple-counterexample guided iterative abstraction refinement: An industrial evaluation. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems (2003)
Groce, A., Peled, D., Yannakakis, M.: Adaptive model checking. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems (2002)
Groce, A., Visser, W.: What went wrong: Explaining counterexamples. In: SPINWorkshop (2003)
Lewis, H.R., Papadimitriou, C.H.: Elements of the Theory of Computation. Prentice Hall Inc., Englewood Cliffs (1998)
Namjoshi, K.: Certifying model checkers. In: 13th International Conference Computer Aided Verification (2001)
Pace, G., Halbwachs, N., Raymond, P.: Counter-example generation in symbolic abstract model-checking. In: 6th International Workshop on Formal Methods for Industrial Critical Systems, Paris, Inria (2001)
Pasareanu, C.S., Dwyer, M.B., Visser, W.: Finding feasible counter-examples when model checking abstracted Java programs. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems (2001)
Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in Cesar. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137. Springer, Heidelberg (1982)
Sai̋di, H.: Model checking guided abstraction and analysis. In: Static Analysis Symposium (2000)
Sander, G.: Graph layout through the VCG tool. In: Tamassia, R., Tollis, I.G. (eds.) GD 1994. LNCS, vol. 894, pp. 194–205. Springer, Heidelberg (1995)
Sekar, R., Ramakrishnan, C.R., Ramakrishnan, I.V., Smolka, S.A.: Model-carrying code: A new paradigm for mobile-code security. In: New Security Paradigms Workshop, Cloudcroft, New Mexico (2001)
XSB. The XSB logic programming system, Available from http://xsb.sourceforge.net
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 IFIP International Federation for Information Processing
About this paper
Cite this paper
Basu, S., Saha, D., Lin, YJ., Smolka, S.A. (2003). Generation of All Counter-Examples for Push-Down Systems. In: König, H., Heiner, M., Wolisz, A. (eds) Formal Techniques for Networked and Distributed Systems - FORTE 2003. FORTE 2003. Lecture Notes in Computer Science, vol 2767. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39979-7_6
Download citation
DOI: https://doi.org/10.1007/978-3-540-39979-7_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20175-5
Online ISBN: 978-3-540-39979-7
eBook Packages: Springer Book Archive