Wolper, Pierre ; Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique (parallélisme et banques de données)
Godefroid, Patrice
Language :
English
Title :
Partial-Order Methods for Temporal Verification
Publication date :
1993
Event name :
4th Intrenational Conference on Concurrency Theory
B. Alpern and F. B. Schneider. Recognizing safety and liveness. Distributed Computing, 2:117-126, 1987.
C. Courcoubetis, M. Vardi, P. Wolper, and M. Yannakakis. Memory efficient algorithms for the verification of temporal properties. Formal Methods in System Design, 1:275-288, 1992.
P. Godefroid, G. J. Holzmann, and D. Pirottin. State space caching revisited. In Proc. 4th Workshop on Computer Aided Verification, Montreal, June 1992.
P. Godefroid. Using partial orders to improve automatic verification methods. In Proc. 2nd Workshop on Computer Aided Verification, volume 531 of Lecture Notes in Computer Science, pages 176-185, Rutgers, June 1990. Springer-Verlag.
P. Godefroid and D. Pirottin. Refining dependencies improves partial-order verification methods. In Proc. 5th Workshop on Computer Aided Verification, Elounda, June 1993. Lecture Notes in Computer Science, Springer-Verlag.
P. Godefroid and P. Wolper. A partial approach to model checking. In Proc. 6th Symp on Logic in Computer Science, pages 406-415, Amsterdam, July 1991.
P. Godefroid and P. Wolper. Using partial orders for the efficient verification of deadlock freedom and safety properties. In Proc. 3rd Workshop on Computer Aided Verification, volume 575 of Lecture Notes in Computer Science, pages 332-342, Aalborg, July 1991. Springer-Verlag.
P. Godefroid and P. Wolper. Using partial orders for the efficient verification of deadlock freedom and safety properties. Formal Methods in System Design, 2(2):149-164, April 1993.
G. J. Holzmann, P. Godefroid, and D. Pirottin. Coverage preserving reduction strategies for reachability analysis. In Proc. 12th International Symposium on Protocol Specification, Testing, and Verification, Lake Buena Vista, Florida, June 1992. North-Holland.
G. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall International Editions, 1991.
S. Katz and D. Peled. Defining conditional independence using collapses. Theoretical Computer Science, 101:337-359, 1992.
A. Mazurkiewicz. Trace theory. In Petri Nets: Applications and Relationships to Other Models of Concurrency, Advances in Petri Nets 1986, Part II; Proceedings of an Advanced Course, volume 255 of Lecture Notes in Computer Science, pages 279-324, 1986.
K. McMillan. Using unfolding to avoid the state explosion problem in the verification of asynchronous circuits. In Proc. 4th Workshop on Computer Aided Verification, Montreal, June 1992.
W. T. Overman. Verification of Concurrent Systems: Function and Timing. PhD thesis, University of California Los Angeles, 1981.
D. Peled. All from one, one for all: on model checking using representatives. In Proc. 5th Workshop on Computer Aided Verification, Elounda, June 1993. Lecture Notes in Computer Science, Springer-Verlag.
D. K. Probst and H. F. Li. Abstract specification, composition and proof of correctness of delay-insensitive circuits and systems. Cs-vlsi-88-2, Department of Computer Science, Concordia University, Montreal, Quebec Canada, 1989.
D. K. Probst and H. F. Li. Using partial-order semantics to avoid the state explosion problem in asynchronous systems. In Proc. 2nd Workshop on Computer Aided Verification, volume 531 of Lecture Notes in Computer Science, pages 146-155, Rutgers, June 1990. Springer-Verlag.
A. Valmari. A stubborn attack on state explosion. In Proc. 2nd Workshop on Computer Aided Verification, volume 531 of Lecture Notes in Computer Science, pages 156-165, Rutgers, June 1990. Springer-Verlag.
A. Valmari. Stubborn sets for reduced state space generation. In Advances in Petri Nets 1990, volume 483 of Lecture Notes in Computer Science, pages 491-515. Springer-Verlag, 1991.
A. Valmari. On-the-fly verification with stubborn sets. In Proc. 5th Workshop on Computer Aided Verification, Elounda, June 1993. Lecture Notes in Computer Science, Springer-Verlag.
M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. Symp on Logic in Computer Science, pages 322-331, Cambridge, June 1986.
P. Wolper. On the relation of programs and computations to models of temporal logic. In B. Banieqbal, H. Barringer, and A. Pnueli, editors, Proc. Temporal Logic in Specification, volume 398, pages 75-123. Lecture Notes in Computer Science, Springer-Verlag, 1989.