On the Existence of Network Invariants for Verifying Parameterized Systems? - Correct System Design: Recent Insights and Advances - page 189

in Computer Science , pages 244{256, New Brunswick, USA, 1996. Springer
Verlag.

BS95. O. Burkart and B. Steen. Composition, decomposition, and model check-

ing of pushdown processes. Nordic Journal of Computing , 2(2):89{125,

1995.

CGJ95. E. M. Clarke, O. Grumberg, and S. Jha. Verifying parameterized networks

using abstraction and regular languages. In Lee and Smolka, editors, Proc.
CONCUR '95, 6 th Int. Conf. on Concurrency Theory , volume 962 of Lec-
ture Notes in Computer Science , pages 395{407. Springer Verlag, 1995.

Dic13. L. E. Dickson. Finiteness of the odd perfect and primitive abundant num-

bers with n distinct prime factors.

Amer.J.Math. , 35:413{422, 1913.

EFM99. J. Esparza, A. Finkel, and R. Mayr. On the verication of broadcast

protocols. In Proc. 14 th IEEE Int. Symp. on Logic in Computer Science ,
1999.

E.A. Emerson and K.S. Namjoshi. Reasoning about rings. In Proc. 22 th
ACM Symp. on Principles of Programming Languages , 1995.

EN95.

Fin94. A. Finkel. Decidability of the termination problem for completely specied

protocols. Distributed Computing , 7(3), 1994.

GS92. S. M. German and A. P. Sistla. Reasoning about systems with many

Journal of the ACM , 39(3):675{735, 1992.

processes.

Hen95. T.A. Henzinger. Hybrid automata with nite bisimulations. In Proc.

ICALP '95 , 1995.

ID99. C. Norris Ip and David L. Dill. Verifying systems with replicated compo-

nents in Mur ' .

Formal Methods in System Design , 14(3), May 1999.

JK95. Bengt Jonsson and Lars Kempe. Verifying safety properties of a class

of innite-state distributed algorithms. In Proc. 7 th Int. Conf. on Com-
puter Aided Verication , volume 939 of Lecture Notes in Computer Science ,
pages 42{53. Springer Verlag, 1995.

JM95. P. Jancar and F. Moller. Checking regular properties of Petri nets. In

Proc. CONCUR '95, 6 th Int. Conf. on Concurrency Theory , pages 348{

362, 1995.
JP93. B. Jonsson and J. Parrow. Deciding bisimulation equivalences for a class of
non-nite-state programs. Information and Computation , 107(2):272{302,
Dec. 1993.
KLL + 97. K.J. Kristoersen, F. Larroussinie, K. G. Larsen, P. Pettersson, and W. Yi.
A compositional proof of a real-time mutual exclusion protocol. In TAP-
SOFT '97 7th International Joint Conference on the Theory and Prac-
tice of Software Development , Lecture Notes in Computer Science, Lille,
France, April 1997. Springer Verlag.
KM89. R.P. Kurshan and K. McMillan. A structural induction theorem for pro-
cesses. In Proc. 8 th ACM Symp. on Principles of Distributed Computing,
Canada , pages 239{247, Edmonton, Alberta, 1989.
KMM + 97. Y. Kesten, O. Maler, M. Marcus, A. Pnueli, and E. Shahar. Symbolic
model checking with rich assertional languages. In O. Grumberg, editor,
Proc. 9 th Int. Conf. on Computer Aided Verication , volume 1254, pages
424{435, Haifa, Israel, 1997. Springer Verlag.

Lam89. L. Lamport. A simple approach to specifying concurrent systems,. Com-

munications of the ACM , 32(1):32{45, Jan. 1989.

LHR97. D. Lesens, N. Halbwachs, and P. Raymond. Automatic verication of

parameterized linear networks of processes. In Proc. 24 th ACM Symp. on
Principles of Programming Languages , 1997.