Specification and verification of the UCLA Unix security kernel
作者： Bruce J. Walker , Richard A. Kemmerer , Gerald J. Popek
关键词:
摘要:
acm.org
sci-hub.se 参考文章(25)
Richard Allen Kemmerer, Formal verification of the ucla security kernel: abstract model, mapping functions, theorem generation, and proofs. University of California, Los Angeles. ,(1979)
David Luckham, Norihisa Suzuki, Automatic program verification V: verification-oriented proof rules for arrays, records and pointers Stanford University. ,(1976) , 10.21236/ADA027455
B. H. Mayoh, Donald Kalish and Richard Montague. Logic. Techniques of formal reasoning . Harcourt, Brace a World, Inc., New York and Burlingame1964, x + 350 pp. Journal of Symbolic Logic. ,vol. 34, pp. 641- 642 ,(1969) , 10.2307/2270857
J. Hartmanis, P. Brinch Hansen, D. Gries, Kathleen Jensen, C. Moler, G. Seegmüller, Niklaus Wirth, N. Wirth, G. Goos, Pascal user manual and report ,(1975)
D. M. Ritchie, K. Thompson, The UNIX Time-Sharing System† Bell System Technical Journal. ,vol. 57, pp. 1905- 1929 ,(1978) , 10.1002/J.1538-7305.1978.TB02136.X
B. W. Lampson, J. J. Horning, R. L. London, J. G. Mitchell, G. J. Popek, Report on the programming language Euclid Sigplan Notices. ,vol. 12, pp. 1- 79 ,(1977) , 10.1145/954666.971189
W.A. Wulf, R.L. London, M. Shaw, An Introduction to the Construction and Verification of Alphard Programs IEEE Transactions on Software Engineering. ,vol. SE-2, pp. 253- 265 ,(1976) , 10.1109/TSE.1976.233830
Gerald J. Popek, A model for verification of data security in operating systems Communications of the ACM. ,vol. 21, pp. 737- 749 ,(1978) , 10.1145/359588.359597
Mary Shaw, William A. Wulf, Ralph L. London, Abstraction and verification in Alphard Communications of the ACM. ,vol. 20, pp. 553- 564 ,(1977) , 10.1145/359763.359782
Richard Montague, Gary Mar, Donald Kalish, Logic : Techniques of Formal Reasoning ,(1964)