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)
Language :
English
Title :
Using partial orders for the efficient verification of deadlock freedom and safety properties
Publication date :
1991
Event name :
3rd International Workshop on Computer Aided Verification, CAV '91
B. Alpern and F. B. Schneider. Recognizing safety and liveness. Distributed Computing, 2: 117-126, 1987.
A. Bouajjani, J.-C. Fernandez, S. Graf, C. Rodriguez, and J. Sifakis. Safety for branching semantics. In Proc. 12th Int. Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science, Springer-Verlag, July 1991.
A. Bouajjani, J. C. Fernandez, and N. Halbwachs. On the verification of safety properties. Technical Report SPECTRE L12, IMAG, Grenoble, March 1990.
J.R. Biichi. On a decision method in restricted second order arithmetic. In Proc. Internat. Congr. Logic, Method and Philos. Sci. 1960, pages 1-12, Stanford, 1962. Stanford University
E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent \ systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2): 244-263, January 1986.
C. Courcoubetis, M. Vardi, P. Wolper, and M. Yannakakis. Memory efficient algorithms for the verification of temporal properties. In Proc. Workshop on Computer Aided Verification, Rutgers, June 1990.
J.C. Fernandez and L. Mounier. On the fly verification of behavioural equivalences and preorders. In Proc. Workshop on Computer Aided Verification, Aalborg, July 1991.
H. Gaifman. Modeling concurrency by partial orders and nonlinear transition systems. In Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency,volume 354 of Lecture Notes in Computer Science, pages 467-488, 1988.
P. Godefroid and F. Kabanza. An efficient reactive planner for synthesizing reactive plans. In Proceedings of AAAI-91, volume 2, pages 640-645, Anaheim, July 1991.
P. Godefroid. Using partial orders to improve automatic verification methods. In Proc. Workshop on Computer Aided Verification, Rutgers, June 1990.
S. Graf and B. Steffen. Using interface specifications for compositional reduction. In Proc. Workshop on Computer Aided Verification, Rutgers, June 1990.
P. Godefroid and P. Wolper. A partial approach to model checking. In Proceedings of the 6th IEEE Symposium on Logic in Computer Science, pages 406-415, Amsterdam, July 1991.
G. Holzmann. An improved protocol reachability analysis technique. Software Practice and Experience, pages 137-161, February 1988.
N. Halbwachs, D. Pilaud, F. Ouabdesselam, and A.C. Glory. Specifying, programming and verifying real-time systems, using a synchronous declarative language. In Workshop on automatic verification methods for finite state systems, volume 407 of Lecture Notes in Computer Science, pages 213-231, Grenoble, June 1989.
C. Jard and T. Jeron. On-line model-checking for finite linear temporal logic specifications. In Workshop on automatic verification methods for finite state systems, volume 407 of Lecture Notes in Computer Science, pages 189-196, Grenoble, June 1989.
C. Jard and T. Jeron. Bounded-memory algorithms for verification on the fly. In Proc. Workshop on Computer Aided Verification, Aalborg, July 1991.
O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In Proceedings of the Twelfth ACM Symposium on Principles of Programming Languages, pages 97-107, New Orleans, January 1985.
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.
Z. Manna and A. Pnueli. Adequate proof principles for invariance and liveness properties of concurrent programs. Science of Computer Programming, 4: 257-289, 1984.
S. Owicki and L. Lamport. Proving liveness properties of concurrent programs. ACM Transactions on Programming Languages and Systems, 4(3): 455-495, July 1982.
D. K. Probst and H. F. Li. Using partial-order semantics to avoid the state explosion problem in asynchronous systems. In Proc. Workshop on Computer Aided Verification, Rutgers, June 1990.
J.P. Quielle and J. Sifakis. Specification and verification of concurrent systems in cesar. In Proc. 5th Int’l Symp. on Programming, volume 137 of Lecture Notes in Computer Science, pages 337-351, 1981.
M.O. Rabin. Decidability of second order theories and automata on infinite trees. Transaction of the AMS, 141: 1-35, 1969.
Shmuel Safra. On the complexity of omega-automata. In Proceedings of the S9th IEEE Symposium on Foundations of Computer Science, White Plains, oct 1988.
A.P. Sistla, M.Y. Vardi, and P. Wolper. The complementation problem for Büchi automata with applications to temporal logic. Theoretical Computer Science, 49: 217-237, 1987.
A. Valmari. Error detection by reduced reachability graph generation. In Proc. 9th International Conference on Application and Theory of Petri Nets, pages 95-112, Venice, 1988.
A. Valmari. Stubborn sets for reduced state space generation. In Proc. 10th International Conference on Application and Theory of Petri Nets, volume 2, pages 1-22, Bonn, 1989.
A. Valmari. A stubborn attack on state explosion. In Proc. Workshop on Computer Aided Verification, Rutgers, June 1990.
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.
