GAMES logo Nodes: Rice
Aachen Bordeaux Edinburgh Paris Rice Uppsala Warsaw Vienna

Task 5: Linear-time model checking

Objectives

UNDERCONSTRUCTION

Material

Background literature

[1] M. Y. Vardi and P. Wolper, An automata-theoretic approach to automatic program verification, in Proc. 1st Symp. on Logic in Computer Science, (Cambridge), pp. 332-344, June 1986.
[ BibTeX ]
[2] M. Y. Vardi, Verification of concurrent programs - the automata-theoretic framework, Annals of Pure and Applied Logic, vol. 51, pp. 79-98, 1991.
[ BibTeX ]
[3] M. Y. Vardi, Probabilistic linear-time model checking: An overview of the automata-theoretic approach, in 5th Int'l Workshop on Formal Methods for Real-Time and Probabilistic Systems (J. P. Katoen, ed.), Lecture Notes in Computer Science 1601, pp. 265-276, Springer-Verlag, 1999.
[ BibTeX ]
[4] C. Courcoubetis, M. Y. Vardi, P. Wolper, and M. Yannakakis, Memory efficient algorithms for the verification of temporal properties, Formal Methods in System Design, vol. 1, pp. 275-288, 1992.
[ BibTeX ]
[5] M. Y. Vardi and P. Wolper, Reasoning about infinite computations, Information and Computation, vol. 115, pp. 1-37, Nov. 1994.
[ BibTeX ]
[6] M. Y. Vardi, An automata-theoretic approach to linear temporal logic, in Logics for Concurrency: Structure versus Automata (F. Moller and G. Birtwistle, eds.), vol. 1043 of Lecture Notes in Computer Science, pp. 238-266, Springer-Verlag, Berlin, 1996.
[ BibTeX ]
[7] M. Y. Vardi, Alternating automata and program verification, in Computer Science Today -Recent Trends and Developments, vol. 1000 of Lecture Notes in Computer Science, pp. 471-485, Springer-Verlag, Berlin, 1995.
[ BibTeX ]
[8] R. Gerth, D. Peled, M. Y. Vardi, and P. Wolper, Simple on-the-fly automatic verification of linear temporal logic, in Protocol Specification, Testing, and Verification (P. Dembiski and M. Sredniawa, eds.), pp. 3-18, Chapman & Hall, Aug. 1995.
[ BibTeX ]
[9] N. Daniele, F. Guinchiglia, and M. Y. Vardi, Improved automata generation for linear temporal logic, in Computer Aided Verification, Proc. 11th International Conference, vol. 1633 of Lecture Notes in Computer Science, pp. 249-260, Springer-Verlag, 1999.
[ BibTeX ]
[10] O. Kupferman and M. Y. Vardi, Model checking of safety properties, Formal methods in System Design, vol. 19, pp. 291-314, Nov. 2001.
[ BibTeX ]
[11] O. Kupferman and M. Y. Vardi, Weak alternating automata are not that weak, ACM Trans. on Computational Logic, vol. 2001, pp. 408-429, July 2001.
[ BibTeX ]