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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
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)
Apt, K.R., Kozen, D.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 22(6), 307–309 (1986)
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)
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)
Ball, T., Rajamani, S.K.: The SLAM toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, Springer, Heidelberg (2001)
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)
Browne, M.C., Clarke, E.M., Grumberg, O.: Reasoning about networks with many identical finite state processes. Inf. Comput. 81(1), 13–31 (1989)
Chandy, K.M., Misra, J.: Proofs of networks of processes. IEEE Transactions on Software Engineering 7(4) (1981)
Clarke, E.M., Grumberg, O.: Avoiding the state explosion problem in temporal logic model checking. In: PODC, pp. 294–303 (1987)
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)
Dams, D., Namjoshi, K.S.: The existence of finite abstractions for branching time model checking. In: LICS (2004)
de Roeve, W-P., et al.: Concurrency Verification: Introduction to Compositional and Noncompositional Proof Methods. Cambridge University Press, Cambridge (2001)
Dijkstra, E.W.: Guarded commands, nondeterminacy, and formal derivation of programs. CACM 18(8) (1975)
Dijkstra, E.W., Scholten, C.S.: Predicate Calculus and Program Semantics. Springer, Heidelberg (1990)
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)
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)
Emerson, E.A., Namjoshi, K.S.: Reasoning about rings. In: ACM Symposium on Principles of Programming Languages (1995)
Flanagan, C., et al.: Modular verification of multithreaded programs. Theor. Comput. Sci. 338(1-3), 153–183 (2005)
Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: POPL, pp. 191–202 (2002)
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)
German, S., Sistla, A.P.: Reasoning about systems with many processes. Journal of the ACM (1992)
Graf, S., Saïdi, H.: Construction of abstract state graphs with. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, Springer, Heidelberg (1997)
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)
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)
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL, pp. 58–70 (2002)
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)
Jones, C.B.: Development methods for computer programs including a notion of interference. PhD thesis, Oxford University (1981)
Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. on Programming Languages and Systems (TOPLAS) (1983)
Kesten, Y., Pnueli, A.: Verification by augmented finitary abstraction. Information and Computation 163(1) (2000)
Kesten, Y., et al.: Symbolic model checking with rich ssertional languages. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, Springer, Heidelberg (1997)
Kesten, Y., Pnueli, A.: Control and data abstraction: The cornerstones of practical formal verification. STTT 2(4), 328–342 (2000)
Kurshan, R.P., McMillan, K.L.: A structural induction theorem for processes. In: PODC, pp. 239–247 (1989)
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)
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)
Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Software Eng. 3(2) (1977)
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)
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)
Owicki, S.S., Gries, D.: Verifying properties of parallel programs: An axiomatic approach. Commun. ACM 19(5), 279–285 (1976)
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)
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)
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)
Suzuki, I.: Proving properties of a ring of finite-state machines. Inf. Process. Lett. 28(4), 213–214 (1988)
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)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Namjoshi, K.S. (2007). Symmetry and Completeness in the Analysis of Parameterized Systems. In: Cook, B., Podelski, A. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2007. Lecture Notes in Computer Science, vol 4349. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69738-1_22
Download citation
DOI: https://doi.org/10.1007/978-3-540-69738-1_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69735-0
Online ISBN: 978-3-540-69738-1
eBook Packages: Computer ScienceComputer Science (R0)