Information Technology Reference
In-Depth Information
[10] M. Dam. CTL* and ECTL* as fragments of the modal mu-calculus.
Theoretical Computer
Science
, 126, 1994.
[11] D. L. Dill. The MurΦ verification system. In
CAV'96
, LNCS. Springer, 1996.
[12] Y. Dong, X. Du, Y.S. Ramakrishna, C. T. Ramkrishnan, I. V. Ramakrishnan, S. A. Smolka,
O. Sokolsky, E. W. Starck, and D. S. Warren. Fighting livelock in the i-protocol: A com-
parative study of verification tools. In
TACAS'99
, LNCS. Springer, 1999.
[13] E. A. Emerson and C.-L. Lei. Modalities for model checking: Branching time strikes back.
Science of Computer Programming
, 8, 1986.
[14] R. Gerth, D. Peled, M. Y. Vardi, and P. Wolper. Simple on-the-fly automatic verification
of linear temporal logic. In
Proceedings 15th Workshop on Protocol Specification, Testing,
and Verification
. North-Holland, 1995.
[15] T. A. Henzinger, O. Kupferman, and S. Qadeer. From Pre-historic to Post-modern symbolic
model checking. In
CAV'98
, LNCS. Springer, 1998.
[16] G. J. Holzmann. The model checker SPIN.
IEEE Transactions on Software Engineering
,
5(23), 1997.
[17] H. Iwashita and T. Nakata.
CTL model checking based on forward state traversal.
In
ICCAD'96
. ACM, 1996.
[18] H. Iwashita, T. Nakata, and F. Hirose. Forward model checking techniques oriented to
buggy design. In
ICCAD'97
. ACM, 1997.
[19] A. Kick.
Generierung von Gegenbeispielen und Zeugen bei der Modellprufung
. PhD thesis,
Fakultat f ur Informatik, Universitat Karlsruhe, 1996.
[20] D. Kozen.
Results on the propositional
µ
-calculus.
Theoretical Computer Science
, 27,
1983.
[21] O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their
linear specification. In
Symposium on Principles of Programming Languages
,NewYork,
1985. ACM.
[22] D. E. Long, A. Browne, E. M. Clarke, S. Jha, and W. R. Marrero. An improved algorithm
for the evaluation of fixpoint expressions. In
CAV'94
, LNCS. Springer, 1994.
[23] K. L. McMillan.
Symbolic Model Checking
. Kluwer, 1993.
[24] J. P. Quielle and J. Sifakis. Specification and verification of concurrent systems in CESAR.
In
Proc. 5th Int. Symp. in Programming
, 1981.
[25] K. Ravi, K. L. McMillan, T. R. Shiple, and F. Somenzi. Approximation and decomposition
of binary decision diagrams. In
DAC'98
. ACM, 1998.
[26] K. Ravi and F. Somenzi. High-density reachability analysis. In
ICCAD'95
. ACM, 1995.
[27] F. Reffel. Modellpr ufung von Unterlogiken von CTL*. Masterthesis, Fakultat f ur Infor-
matik, Universitat Karlsruhe, 1996.
[28] C. Stirling and D. Walker. Local model checking in the modal mu-calculus.
Theoretical
Computer Science
, 89, 1991.
[29] M. Y. Vardi and P. Wolper. Reasoning about infinite computations.
Information and Com-
putation
, 115(1), 1994.
Search WWH ::
Custom Search