A computer-checked verification of Milner's scheduler

1. J.C.M. Baeten and W.P. Weijland. Process Algebra. Cambridge Tracts in Theoretical Computer Science 18. Cambridge University Press, 1990.

   Google Scholar 

2. M. Bezem and J.F. Groote. A formal verification of the alternating bit protocol in the calculus of constructions. Technical Report Logic Group Preprint Series No. 88, Utrecht University, 1993.

   Google Scholar 

3. T. Coquand and G. Huet. The calculus of constructions. Information and Control, 76:95–120, 1988.

   Google Scholar 

4. G. Dowek, A. Felty, H. Herbelin, G. Huet, C. Murthy, C. Parent, C. Paulin-Mohring, and B. Werner. The Coq proof assistant user's guide. Version 5.8. Technical report, INRIA — Rocquencourt, May 1993.

   Google Scholar 

5. H. Ehrig and B. Mahr. Fundamentals of algebraic specifications I, volume 6 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag, 1985.

   Google Scholar 

6. J.-C. Fernandez, A. Kerbrat and L. Mounier. Symbolic Equivalence Checking. In C. Courcoubetis, editor, Proceedings of the 5th International Conference, CAV '93, Elounda, Greece, volume 697 of Lecture Notes in Computer Science, pages 85–97. Springer-Verlag, 1993.

   Google Scholar 

7. J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types, volume 7 of Cambridge tracts in theoretical computer science. Cambridge University Press, Cambridge, 1989.

   Google Scholar 

8. R.J. van Glabbeek and W.P. Weijland. Branching time and abstraction in bisimulation semantics (extended abstract). In G.X. Ritter, editor, Information Processing 89, pages 613–618. North-Holland, 1989.

   Google Scholar 

9. J.F. Groote and H. Korver. A correctness proof of the bakery protocol in μCRL. Technical Report Logic Group Preprint Series No. 80, Utrecht University, 1992.

   Google Scholar 

10. J.F. Groote and J.C. van de Pol. A bounded retransmission protocol for large data packets. A case study in computer checked verification. Technical Report 100, Logic Group Preprint Series, Utrecht University, October 1993.

    Google Scholar 

11. J.F. Groote and A. Ponse. The syntax and semantics of μCRL. Technical Report CS-R9076, CWI, Amsterdam, 1990.

    Google Scholar 

12. J.F. Groote and A. Ponse. Proof theory for μCRL. Technical Report CS-R9138, CWI, Amsterdam, 1991.

    Google Scholar 

13. J.F. Groote and A. Ponse. μCRL: A base for analysing processes with data. In E. Best and G. Rozenberg, editors, Proceedings 3rd Workshop on Concurrency and Compositionality, Goslar, GMD-Studien Nr. 191, pages 125–130. Universität Hildesheim, 1991.

    Google Scholar 

14. L. Helmink, M.P.A. Sellink, and F. Vaandrager. Proof-checking a data link protocol. 1993. To appear.

    Google Scholar 

15. H. Korver and J. Springintveld. A Computer-Checked Verification of Milner's Scheduler. Technical Report Logic Group Preprint Series No. 101, Utrecht University, November, 1993. Full version.

    Google Scholar 

16. R. Milner. Communication and Concurrency. Prentice-Hall International, Englewood Cliffs, 1989.

    Google Scholar 

17. C. Paulin-Mohring. Inductive definitions in the system Coq. Rules and properties. In M. Bezem and J.F. Groote, editors, Proceedings of the 1st International Conference on Typed Lambda Calculi and Applications, TLCA '93, Utrecht, The Netherlands, volume 664 of Lecture Notes in Computer Science, pages 328–345. Springer-Verlag, 1993.

    Google Scholar 

18. M.P.A. Sellink. Verifying process algebra proofs in type theory. Technical Report Logic Group Preprint Series No. 87, Utrecht University, 1993.

    Google Scholar 

19. N.V. Stenning. A data transfer protocol. Computer Networks. 1:99–110, 1976.

    Google Scholar 

20. A.S. Tanenbaum. Computer networks. Prentice-Hall International, Englewood Cliffs, 1989.

    Google Scholar 

Download references