Search from the table of contents of 2.5 million books
Advanced Search (Beta)
Home > Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs' 96, Turku, Finland, August 26 - 30, 1996, Proceedings > Towards applying the composition principle to verify a microkernel operating system
Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs' 96, Turku, Finland, August 26 - 30, 1996, Proceedings |
Joakim von Wright; Jim Grundy; John Harrison
Springer Berlin Heidelberg
Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs' 96, Turku, Finland, August 26 - 30, 1996, Proceedings
Towards applying the composition principle to verify a microkernel operating system
Authors

Mark R. Heckman; Cui Zhang; Brian R. Becker; Dave Peticolas; Karl N. Levitt; Ron A. Olsson

ARI Id

1664385591918_1460268

Access

Not Available Free

Pages

235-250

DOI

10.1007/BFb0105408

Chapter URL

https://rd.springer.com/chapter/10.1007/BFb0105408

Table of Contents of Book
Showing 1 to 20 of 30 entries
Chapters/HeadingsAuthor(s)PagesInfo
Front Matter
Translating specifications in VDM-SL to PVS
Sten Agerholm
1-16
A comparison of HOL and ALF formalizations of a categorical coherence theorem
Sten Agerholm; Ilya Beylin; Peter Dybjer
17-32
Modeling a hardware synthesis methodology in isabelle
David Basin; Stefan Friedrich
33-50
Inference rules for programming languages with side effects in expressions
Paul E. Black; Phillip J. Windley
51-60
Deciding cryptographic protocol adequacy with HOL: The implementation
Stephen H. Brackin
61-76
Proving liveness of fair transition systems
Holger Busch
77-92
Program derivation using the refinement calculator
Michael Butler; Thomas Långbacka
93-108
A proof tool for reasoning about functional programs
Graham Collins
109-124
Coq and hardware verification: A case study
Solange Coupet-Grimal; Line Jakubiec
125-139
Elements of mathematical analysis in PVS
Bruno Dutertre
141-156
Implementation issues about the embedding of existing high level synthesis algorithms in HOL
Dirk Eisenbiegler; Christian Blumenröhr; Ramayya Kumar
157-172
Five axioms of alpha-conversion
Andrew D. Gordon; Tom Melham
173-190
Set theory, higher order logic or both?
Mike Gordon
191-201
A mizar mode for HOL
John Harrison
203-220
Stålmarck’s algorithm as a HOL derived rule
John Harrison
221-234
Towards applying the composition principle to verify a microkernel operating system
Mark R. Heckman; Cui Zhang; Brian R. Becker; Dave Peticolas; Karl N. Levitt; Ron A. Olsson
235-250
A modular coding of UNITY in COQ
Barbara Heyd; Pierre Crégut
251-266
Importing mathematics from HOL into Nuprl
Douglas J. Howe
267-281
A structure preserving encoding of Z in isabelle/HOL
Kolyang; T. Santen; B. Wolff
283-298
Chapters/HeadingsAuthor(s)PagesInfo
Showing 1 to 20 of 30 entries
Similar Books
Similar Chapters
Similar Thesis

Similar News

Similar Articles
Similar Article Headings