Using partial orders for the efficient verification of deadlock freedom and safety properties

1. B. Alpern and F. B. Schneider. Recognizing safety and liveness. Distributed Computing, 2:117–126, 1987.

   Google Scholar 

2. 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.

   Google Scholar 

3. A. Bouajjani, J. C. Fernandez, and N. Halbwachs. On the verification of safety properties. Technical Report SPECTRE L12, IMAG, Grenoble, March 1990.

   Google Scholar 

4. J.R. Büchi. 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 Press.

   Google Scholar 

5. 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.

   Google Scholar 

6. 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.

   Google Scholar 

7. 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.

   Google Scholar 

8. 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.

   Google Scholar 

9. 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.

   Google Scholar 

10. P. Godefroid. Using partial orders to improve automatic verification methods. In Proc. Workshop on Computer Aided Verification, Rutgers, June 1990.

    Google Scholar 

11. S. Graf and B. Steffen. Using interface specifications for compositional reduction. In Proc. Workshop on Computer Aided Verification, Rutgers, June 1990.

    Google Scholar 

12. 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.

    Google Scholar 

13. G. Holzmann. An improved protocol reachability analysis technique. Software Practice and Experience, pages 137–161, February 1988.

    Google Scholar 

14. 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 autosmatic verification methods for finite state systems, volume 407 of Lecture Notes in Computer Science, pages 213–231, Grenoble, June 1989.

    Google Scholar 

15. 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.

    Google Scholar 

16. C. Jard and T. Jeron. Bounded-memory algorithms for verification on the fly. In Proc. Workshop on Computer Aided Verification, Aalborg, July 1991.

    Google Scholar 

17. 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.

    Google Scholar 

18. 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.

    Google Scholar 

19. Z. Manna and A. Pnueli. Adequate proof principles for invariance and liveness properties of concurrent programs. Science of Computer Programming, 4:257–289, 1984.

    Google Scholar 

20. S. Owicki and L. Lamport. Proving liveness properties of concurrent programs. ACM Transactions on Programming Languages and Systems, 4(3):455–495, July 1982.

    Article  Google Scholar 

21. 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.

    Google Scholar 

22. 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.

    Google Scholar 

23. M.O. Rabin. Decidability of second order theories and automata on infinite trees. Transaction of the AMS, 141:1–35, 1969.

    Google Scholar 

24. Shmuel Safra. On the complexity of omega-automata. In Proceedings of the 29th IEEE Symposium on Foundations of Computer Science, White Plains, oct 1988.

    Google Scholar 

25. 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.

    Google Scholar 

26. 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.

    Google Scholar 

27. 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.

    Google Scholar 

28. A. Valmari. A stubborn attack on state explosion. In Proc. Workshop on Computer Aided Verification, Rutgers, June 1990.

    Google Scholar 

29. 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.

    Google Scholar 

Download references