Check out the new USENIX Web site.

next up previous
Next: About this document Up: Safe Kernel Extensions Without Previous: Acknowledgements


BERSHAD, B., SAVAGE, S., PARDYAK, P., SIRER, E. G., BECKER, D., FIUCZYNSKI, M., CHAMBERS, C., AND EGGERS, S. Extensibility, safety and performance in the SPIN operating system. In Symposium on Operating System Principles (Dec. 1995), pp. 267-284.

BOYER, R. S., AND YU, Y. Automated proofs of object code for a widely used microprocessor. J. ACM 43, 1 (Jan. 1996), 166-192.

CLUTTERBUCK, D., AND CARR´E, B. The verification of low-level code. IEEE Software Engineering Journal 3, 3 (May 1988), 97-111.

CONSTABLE, R. L., ALLEN, S. F., BROMLEY, H. M., CLEAVELAND, W. R., CREMER, J. F., HARPER, R. W., HOWE, D. J., KNOBLOCK, T. B., MENDLER, N. P., PANANGADEN, P., SASAKI, J. T., AND SMITH, S. F. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, 1986.

DIJKSTRA, E. W. Guarded commands, nondeterminancy and formal derivation of programs. Communications of the ACM 18 (1975), 453-457.

FLOYD, R. W. Assigning meanings to programs. In Mathematical Aspects of Computer Science, J. T. Schwartz, Ed. American Mathematical Society, 1967, pp. 19-32.

HARPER, R., HONSELL, F., AND PLOTKIN, G. A framework for defining logics. Journal of the Association for Computing Machinery 40, 1 (Jan. 1993), 143-184.

HOARE, C. A. R. An axiomatic basis for computer programming. Communications of the ACM 12 (1969), 567-580.

HSIEH, W. C., FIUCZYNSKI, M. E., GARRETT, C., SAVAGE, S., BECKER, D., AND BERSHAD, B. N. Language support for extensible operating systems. In The Inaugural Workshop on Compiler Support for Systems Software (Feb. 1996), pp. 127-133.

LEE, P., AND LEONE, M. Optimizing ML with run-time code generation. In PLDI'96 Conference on Programming Language Design and Implementation (May 1996), pp. 137-148.

MARTIN-LöF, P. A theory of types. Technical Report 71-3, Department of Mathematics, University of Stockholm, 1971.

MCCANNE, S. The Berkeley Packet Filter man page. BPF distribution available at, May 1991.

MCCANNE, S., AND JACOBSON, V. The BSD packet filter: A new architecture for user-level packet capture. In The Winter 1993 USENIX Conference (Jan. 1993), USENIX Association, pp. 259-269.

MILNER, R., TOFTE, M., AND HARPER, R. The Definition of Standard ML. MIT Press, Cambridge, Massachusetts, 1990.

MOGUL, J. C., RASHID, R. F., AND ACCETTA, M. J. The packet filter: An efficient mechanism for user-level network code. In ACM Symposium on Operating Systems Principles (Nov. 1987), ACM Press, pp. 39-51. An updated version is available as DEC WRL Research Report 87/2.

NECULA, G. C., AND LEE, P. Proof-carrying code. Technical Report CMU-CS-96-165, Computer Science Department, Carnegie Mellon University, Sept. 1996. Also appeared as FOX memorandum CMU-CS-FOX-96-03.

NELSON, G. Systems Programming with MODULA-3. Prentice-Hall, 1991.

SIRER, E. G., SAVAGE, S., PARDYAK, P., DEFOUW, G. P., AND BERSHAD, B. N. Writing an operating system with Modula-3. In The Inaugural Workshop on Compiler Support for Systems Software (Feb. 1996), pp. 134-140.

SITES, R. L. Alpha Architecture Reference Manual. Digital Press, 1992.

SUN MICROSYSTEMS. The Java language specification. Available as, 1995.

SUN MICROSYSTEMS. The Java Virtual Machine specification. Available as, 1995.

TARDITI, D., MORRISETT, J. G., CHENG, P., STONE, C., HARPER, R., AND LEE, P. TIL: A type-directed optimizing compiler for ML. In PLDI'96 Conference on Programming Language Design and Implementation (May 1996), pp. 181-192.

WAHBE, R., LUCCO, S., ANDERSON, T. E., AND GRAHAM, S. L. Efficient software-based fault isolation. In 14th ACM Symposium on Operating Systems Principles (Dec. 1993), ACM, pp. 203-216.

WALLACH, D. A., ENGLER, D., AND KAASHOEK, M. F. ASHs : Application-specific handlers for high-performance messaging. In ACM SIGCOMM'96 (Oct. 1996), vol. 26, ACM.

Peter Lee
Tue Sep 17 15:37:44 EDT 1996