Shuvendu K. Lahiri
Skip Abstract Section
Abstract
Predicate abstraction provides a powerful tool for verifying properties of infinite-state systems using a combination of a decision procedure for a subset of first-order logic and symbolic methods originally developed for finite-state model checking. We consider models containing first-order state variables, where the system state includes mutable functions and predicates. Such a model can describe systems containing arbitrarily large memories, buffers, and arrays of identical processes. We describe a form of predicate abstraction that constructs a formula over a set of universally quantified variables to describe invariant properties of the first-order state variables. We provide a formal justification of the soundness of our approach and describe how it has been used to verify several hardware and software designs, including a directory-based cache coherence protocol.
- Apt, K. R. and Kozen, D. 1986. Limits for automatic verification of finite-state concurrent systems. Inform. Proces. Lett. 22, 5, 307--309. Google Scholar
Digital Library
- Arons, T. and Pnueli, A. 1999. Verifying Tomasulo's algorithm by Refinement. In Proceedings of the Conference on VLSI Design Conference (VLSI). Google ScholarDigital Library
- Arons, T., Pnueli, A., Ruah, S., Zhu, Y., and Zuck, L. 2001. Parameterized verification with automatically computed inductive assertions. In Proceedings of the Conference on Computer-Aided Verification (CAV), G. Berry, H. Comon, and A. Finkel, Eds. Lecture Notes in Computer Science, vol. 2102. 221--234. Google ScholarDigital Library
- Ball, T., Majumdar, R., Millstein, T., and Rajamani, S. K. 2001. Automatic predicate abstraction of C programs. In Programming Language Design and Implementation (PLDI). Snowbird, Utah. SIGPLAN Notices, 36, 5. Google ScholarDigital Library
- Baukus, K., Lakhnech, Y., and Stahl, K. 2002. Parameterized Verification of a Cache Coherence Protocol: Safety and Liveness. In Proceedings of the International Conference on Verification, Model Checking, and Abstract Interpretation, (VMCAI), A. Cortesi, Ed. Lecture Notes in Computer Science, vol. 2294. 317--330. Google ScholarDigital Library
- Börger, E., Grädel, E., and Gurevich, Y. 1997. The Classical Decision Problem. Springer-Verlag.Google Scholar
- Bouajjani, A., Jonsson, B., Nilsson, M., and Touili, T. 2000. Regular model checking. In Computer-Aided Verification (CAV), A. Emerson and P. Sistla, Eds. Lecture Notes in Computer Science, vol. 1855. Springer-Verlag, 403--418. Google ScholarDigital Library
- Bryant, R. E., Lahiri, S. K., and Seshia, S. A. 2002a. Deciding CLU Logic formulas via Boolean and Pseudo-Boolean encodings. In Proceedings of the International Workshop on Constraints in Formal Verification (CFV).Google Scholar
- Bryant, R. E., Lahiri, S. K., and Seshia, S. A. 2002b. Modeling and Verifying Systems using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions. In Proceedings of the International Conference on Computer-Aided Verification (CAV), E. Brinksma and K. G. Larsen, Eds. Lecture Notes in Computer Science, vol. 2404. 78--92. Google ScholarDigital Library
- Buchi, J. R. 1960. Weak second-order arithmetic and finite automata. Z. Math. Logik Grundl. Math. 6, 66--92.Google ScholarCross Ref
- Burch, J. R. and Dill, D. L. 1994. Automated verification of pipelined microprocessor control. In Proceedings of the International Conference on Computer-Aided Verification (CAV), D. Dill, Ed. Lecture Notes in Computer Science, vol. 818. 68--80. Google ScholarDigital Library
- Chaki, S., Clarke, E. M., Groce, A., Jha, S., and Veith, H. 2003. Modular Verification of Software Components in C. In Proceedings of the International Conference on Software Engineering (ICSE). IEEE Computer Society, 385--395. Google ScholarDigital Library
- Clarke, E. M., Grumberg, O., and Long, D. E. 1992. Model checking and abstraction. In Processings of the International Conference on ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL),. 342--354. Google ScholarDigital Library
- Cousot, P. and Cousot, R. 1977. Abstract interpretation: A Unified Lattice Model for the Static Analysis of Programs by Construction or Approximation of Fixpoints. In Proceedings of the Symposium on Principles of Programming Languages (POPL). ACM Press. Google ScholarDigital Library
- Das, S. and Dill, D. 2001. Successive approximation of abstract transition relations. In IEEE Symposium on Logic in Computer Science(LICS). IEEE Computer Society. Google ScholarDigital Library
- Das, S., Dill, D., and Park, S. 1999. Experience with predicate abstraction. In Proceedings of the Conference on Computer-Aided Verification (CAV). Lecture Notes in Computer Science, vol. 1633. Springer-Verlag. Google ScholarDigital Library
- Das, S. and Dill, D. L. 2002. Counter-example based predicate discovery in predicate abstraction. In Proceedings of the International Conference on Formal Methods in Computer-Aided Design (FMCAD), M. D. Aagaard and J. W. O'Leary, Eds. Lecture Notes in Computer Science, vol. 2517. 19--32. Google ScholarDigital Library
- Dijkstra, E. W. 1975. Guarded commands, nondeterminacy and formal derivation of programs. Comm. ACM 18, 453--457. Google ScholarDigital Library
- Emerson, E. A. and Kahlon, V. 2000. Reducing model checking of the many to the few. In Proceedings of the International Conference on Automated Deduction, D. A. McAllester, Ed. 1831. 236--254. Google ScholarDigital Library
- Emerson, E. A. and Kahlon, V. 2003. Exact and efficient verification of parameterized cache coherence protocols. In Proceedings of the international Conference on Correct Hardware Design and Verification Methods (CHARME), D. Geist and E. Tronci, Eds. Lecture Notes in Computer Science, vol. 2860. 247--262.Google Scholar
- Emerson, E. A. and Namjoshi, K. S. 1995. Reasoning about rings. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). 85--94. Google ScholarDigital Library
- Flanagan, C. and Qadeer, S. 2002. Predicate abstraction for software verification. In Proceedings of the Symposium on Principles of Programming Languages (POPL), J. Launchbury and J. C. Mitchell, Eds. ACM Press, 191--202. Google ScholarDigital Library
- German, S. Personal communication.Google Scholar
- German, S. M. and Sistla, A. P. 1992. Reasoning about systems with many processes. J. ACM 39, 3, 675--735. Google ScholarDigital Library
- Graf, S. and Saïdi, H. 1997. Construction of abstract state graphs with PVS. In Proceedings of the international Conference on Computer-Aided Verification (CAV), O. Grumberg, Ed. Lecture Notes in Computer Science, vol. 1254. Springer-Verlag. Google ScholarDigital Library
- Henzinger, T. A., Jhala, R., Majumdar, R., and Sutre, G. 2002. Lazy Abstraction. In Proceedings of the international Conference on Symposium on Principles of Programming Languages (POPL), J. Launchbury and J. C. Mitchell, Eds. ACM Press, 58--70. Google ScholarDigital Library
- Hosabettu, R., Gopalakrishnan, G., and Srivas, M. 1999. Proof of correctness of a processor with reorder buffer using the completion function approach. In Proceedings of the international Conference on Computer-Aided Verification (CAV). LNCS.Google Scholar
- Ip, C. N. and Dill, D. L. 1996. Verifying systems with replicated components in Murϕ. In Proceedings of the International Conference on Computer-Aided Verification (CAV), R. Alur and T. A. Henzinger, Eds. Lecture Notes in Computer Science, vol. 1102. Springer-Verlag, 147--158. Google ScholarDigital Library
- Kesten, Y., Maler, O., Marcus, M., Pnueli, A., and Shahar, E. 1997. Symbolic model checking with rich assertional languages. In Proceedings of the International Conference on Computer-Aided Verification (CAV '97), O. Grumberg, Ed. Lecture Notes in Computer Science, vol. 1254. Springer-Verlag, 424--435. Google ScholarDigital Library
- Lahiri, S. K. 2004. Unbounded system verification using decision procedures and predicate abstraction. PhD thesis, Carnegie Mellon University. Google ScholarDigital Library
- Lahiri, S. K. and Bryant, R. E. 2004a. Constructing Quantified Invariants via Predicate Abstraction. In Proceedings of the Conference on Verification, Model Checking and Abstract Interpretation (VMCAI), G. Levi and B. Steffen, Eds. Lecture Notes in Computer Science, vol. 2937. 267--281.Google Scholar
- Lahiri, S. K. and Bryant, R. E. 2004b. Indexed Predicate Discovery for Unbounded System Verification. In Proceedings of the International Conference on Computer Aided Verification (CAV). To appear.Google Scholar
- Lahiri, S. K., Bryant, R. E., and Cook, B. 2003. A symbolic approach to predicate abstraction. In Proceedings of the International Conference on Computer-Aided Verification (CAV), W. A. Hunt, Jr. and F. Somenzi, Eds. Lecture Notes in Computer Science, vol. 2725. Springer-Verlag, 141--153.Google Scholar
- Lahiri, S. K., Seshia, S. A., and Bryant, R. E. 2002. Modeling and verification of out-of-order microprocessors in UCLID. In Proceedings of the International Conference on Formal Methods in Computer-Aided Design (FMCAD), J. W. O. M. Aagaard, Ed. Lecture Notes in Computer Science, vol. 2517. Springer-Verlag, 142--159. Google ScholarDigital Library
- Lamport, L. 1974. A new solution of Dijkstra's concurrent programming problem. Comm. ACM 17, 453--455. Google ScholarDigital Library
- McMillan, K. 1998. Verification of an implementation of Tomasulo's algorithm by compositional model checking. In Proceedings of the International Conference on Computer-Aided Verification (CAV), A. J. Hu and M. Y. Vardi, Eds. Lecture Notes in Computer Science, vol. 1427. 110--121. Google ScholarDigital Library
- McMillan, K., Qadeer, S., and Saxe, J. 2000. Induction in compositional model checking. In Proceedings of the International Conference on Computer-Aided Verification (CAV), A. Emerson and P. Sistla, Eds. Lecture Notes in Computer Science, vol. 1855. Springer-Verlag. Google ScholarDigital Library
- Perkins, C., Royer, E., and Das, S. 2002. Ad hoc on demand distance vector (aodv) routing. In IETF Draft., http://www.ietf.org/internet-drafts/draft-ietf-manet-aodv-10.txt. North-Holland, Amsterdam. Google ScholarDigital Library
- Peterson, G. L. 1981. Myths about the mutual exclusion problem. Inform. Proces. Lett. 12, 3, 115--116.Google ScholarCross Ref
- Pnueli, A., Ruah, S., and Zuck, L. 2001. Automatic deductive verification with invisible invariants. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), T. Margaria and W. Yi, Eds. Lecture Notes in Computer Science, Vol. 2031. 82--97. Google ScholarDigital Library
- Saïdi, H. and Shankar, N. 1999. Abstract and model check while you prove. In Proceedings of the International Conference on Computer-Aided Verification, N. Halbwachs and D. Peled, Eds. Lecture Notes in Computer Science, vol. 1633. Springer-Verlag, 443--454. Google ScholarDigital Library
- Strichman, O., Seshia, S. A., and Bryant, R. E. 2002. Deciding Separation Formulas with SAT. In Proceedings of the International Conference on Computer-Aided Verification (CAV), E. Brinksma and K. G. Larsen, Eds. Lecture Notes in Computer Science, vol. 2404. 209--222. Google ScholarDigital Library
- Thomas, W. 1990. Automata on infinite objects. In Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics. Google ScholarDigital Library
Index Terms
- Predicate abstraction with indexed predicates
Recommendations
Combining Theorem Proving with Model Checking through Predicate Abstraction
This article presents a procedure for proving invariants of infinite-state reactive systems using a combination of two formal verification techniques: theorem proving and model checking. This method uses term rewriting on the definition of the target ...
Predicate abstraction in a program logic calculus
Predicate abstraction is a form of abstract interpretation where the abstract domain is constructed from a finite set of predicates over the variables of the program. This paper explores a way to integrate predicate abstraction into a calculus for ...
Modeling Predicate Abstraction of Timed Automata in PVS
ITHINGSCPSCOM '11: Proceedings of the 2011 International Conference on Internet of Things and 4th International Conference on Cyber, Physical and Social ComputingIn this paper, we propose a mechanized framework for formal verification of real-time systems based on predicate abstraction in PVS (Prototype Verification System) based on timed automata model. This framework is composed by two parts: one for modeling ...
Comments