Advertisement

Symmetry and Completeness in the Analysis of Parameterized Systems

  • Kedar S. Namjoshi
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4349)

Abstract

It is shown that the cutoff method—which summarizes a parameterized system by a finite set of its instances—is complete for proving safety properties. This implies completeness of other, less stringent, proof methods for parameterized verification. It is shown that the cutoff method is equivalent to determining a (parameterized) inductive invariant. The second part of the paper describes a new algorithm to construct universally quantified, parameterized inductive invariants. This algorithm is shown to compute the strongest invariant of a given shape, and is complete under certain conditions. A key observation is a previously unnoticed connection between inductiveness, small model theorems, and compositional analysis.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Abdulla, P.A., et al.: Handling global conditions in parameterized system verification. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 134–145. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  2. 2.
    Apt, K.R., Kozen, D.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 22(6), 307–309 (1986)CrossRefMathSciNetGoogle Scholar
  3. 3.
    Arons, T., et al.: Tamarah Arons, Amir Pnueli, Sitvanit Ruah, Jiazhao Xu, and Lenore D. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 221–234. Springer, Heidelberg (2001)Google Scholar
  4. 4.
    Balaban, I., et al.: IIV: An invisible nvariant verifier. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 408–412. Springer, Heidelberg (2005)Google Scholar
  5. 5.
    Ball, T., Rajamani, S.K.: The SLAM toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, Springer, Heidelberg (2001)Google Scholar
  6. 6.
    Bradley, A.R., Manna, Z., Sipma, H.B.: What’s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 427–442. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  7. 7.
    Browne, M.C., Clarke, E.M., Grumberg, O.: Reasoning about networks with many identical finite state processes. Inf. Comput. 81(1), 13–31 (1989)zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    Chandy, K.M., Misra, J.: Proofs of networks of processes. IEEE Transactions on Software Engineering 7(4) (1981)Google Scholar
  9. 9.
    Clarke, E.M., Grumberg, O.: Avoiding the state explosion problem in temporal logic model checking. In: PODC, pp. 294–303 (1987)Google Scholar
  10. 10.
    Clarke, E.M., Talupur, M., Veith, H.: Environment abstraction for parameterized verification. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 126–141. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  11. 11.
    Dams, D., Namjoshi, K.S.: The existence of finite abstractions for branching time model checking. In: LICS (2004)Google Scholar
  12. 12.
    de Roeve, W-P., et al.: Concurrency Verification: Introduction to Compositional and Noncompositional Proof Methods. Cambridge University Press, Cambridge (2001)Google Scholar
  13. 13.
    Dijkstra, E.W.: Guarded commands, nondeterminacy, and formal derivation of programs. CACM 18(8) (1975)Google Scholar
  14. 14.
    Dijkstra, E.W., Scholten, C.S.: Predicate Calculus and Program Semantics. Springer, Heidelberg (1990)zbMATHGoogle Scholar
  15. 15.
    Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: McAllester, D. (ed.) Automated Deduction - CADE-17. LNCS, vol. 1831, Springer, Heidelberg (2000)CrossRefGoogle Scholar
  16. 16.
    Emerson, E.A., Namjoshi, K.S.: Automatic verification of parameterized synchronous systems (extended abstract). In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 87–98. Springer, Heidelberg (1996)Google Scholar
  17. 17.
    Emerson, E.A., Namjoshi, K.S.: Reasoning about rings. In: ACM Symposium on Principles of Programming Languages (1995)Google Scholar
  18. 18.
    Flanagan, C., et al.: Modular verification of multithreaded programs. Theor. Comput. Sci. 338(1-3), 153–183 (2005)zbMATHCrossRefMathSciNetGoogle Scholar
  19. 19.
    Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: POPL, pp. 191–202 (2002)Google Scholar
  20. 20.
    Flanagan, C., Qadeer, S.: Thread-modular model checking. In: Ball, T., Rajamani, S.K. (eds.) Model Checking Software. LNCS, vol. 2648, pp. 213–224. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  21. 21.
    German, S., Sistla, A.P.: Reasoning about systems with many processes. Journal of the ACM (1992)Google Scholar
  22. 22.
    Graf, S., Saïdi, H.: Construction of abstract state graphs with. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, Springer, Heidelberg (1997)Google Scholar
  23. 23.
    Henzinger, T.A., et al.: Temporal-safety proofs for systems code. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, Springer, Heidelberg (2002)Google Scholar
  24. 24.
    Henzinger, T.A., et al.: Thread-modular abstraction refinement. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 262–274. Springer, Heidelberg (2003)Google Scholar
  25. 25.
    Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL, pp. 58–70 (2002)Google Scholar
  26. 26.
    Jhala, R., McMillan, K.L.: A practical and complete approach to predicate refinement. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol. 3920, pp. 459–473. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  27. 27.
    Jones, C.B.: Development methods for computer programs including a notion of interference. PhD thesis, Oxford University (1981)Google Scholar
  28. 28.
    Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. on Programming Languages and Systems (TOPLAS) (1983)Google Scholar
  29. 29.
    Kesten, Y., Pnueli, A.: Verification by augmented finitary abstraction. Information and Computation 163(1) (2000)Google Scholar
  30. 30.
    Kesten, Y., et al.: Symbolic model checking with rich ssertional languages. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, Springer, Heidelberg (1997)Google Scholar
  31. 31.
    Kesten, Y., Pnueli, A.: Control and data abstraction: The cornerstones of practical formal verification. STTT 2(4), 328–342 (2000)zbMATHCrossRefGoogle Scholar
  32. 32.
    Kurshan, R.P., McMillan, K.L.: A structural induction theorem for processes. In: PODC, pp. 239–247 (1989)Google Scholar
  33. 33.
    Lahiri, S.K., Bryant, R.E.: Constructing quantified invariants via predicate abstraction. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 267–281. Springer, Heidelberg (2004)Google Scholar
  34. 34.
    Lahiri, S.K., Bryant, R.E.: Indexed predicate discovery for unbounded system verification. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 135–147. Springer, Heidelberg (2004)Google Scholar
  35. 35.
    Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Software Eng. 3(2) (1977)Google Scholar
  36. 36.
    Lazic, R., Nowak, D.: A unifying approach to data-independence. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 581–595. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  37. 37.
    Namjoshi, K.S., Kurshan, R.P.: Syntactic program transformations for automatic abstraction. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, Springer, Heidelberg (2000)Google Scholar
  38. 38.
    Owicki, S.S., Gries, D.: Verifying properties of parallel programs: An axiomatic approach. Commun. ACM 19(5), 279–285 (1976)zbMATHCrossRefMathSciNetGoogle Scholar
  39. 39.
    Pnueli, A., Ruah, S., Zuck, L.D.: Automatic deductive verification with invisible invariants. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol. 2031, pp. 82–97. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  40. 40.
    Pnueli, A., Shahar, E.: A platform for combining deductive with algorithmic verification. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 184–195. Springer, Heidelberg (1996)Google Scholar
  41. 41.
    Pnueli, A., Shahar, E., Zuck, L.D.: Network invariants in action. In: Brim, L., et al. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 101–115. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  42. 42.
    Suzuki, I.: Proving properties of a ring of finite-state machines. Inf. Process. Lett. 28(4), 213–214 (1988)zbMATHCrossRefGoogle Scholar
  43. 43.
    Wolper, P., Lovinfosse, V.: Verifying properties of large sets of processes with network invariants. In: Sifakis, J. (ed.) Automatic Verification Methods for Finite State Systems. LNCS, vol. 407, pp. 68–80. Springer, Heidelberg (1990)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • Kedar S. Namjoshi
    • 1
  1. 1.Bell Labs 

Personalised recommendations