References

  1. David Cock, Gerwin Klein & Thomas Sewell (2008): Secure Microkernels, State Monads and Scalable Refinement. In: Otmane Ait Mohamed, César Muñoz & Sofiène Tahar: 21st TPHOLs, LNCS 5170. Springer-Verlag, Montreal, Canada, pp. 167–182.
  2. Ernie Cohen, Markus Dahlweid, Mark Hillebrand, Dirk Leinenbach, MichałMoskal, Thomas Santen, Wolfram Schulte & Stephan Tobies (2009): VCC: A Practical System for Verifying Concurrent C. In: Stefan Berghofer, Tobias Nipkow, Christian Urban & Markus Wenzel: 22nd TPHOLs, LNCS 5674. Springer-Verlag, Munich, Germany, pp. 23–42.
  3. C. A. R. Hoare (1983): An axiomatic basis for computer programming. Commun. ACM 26(1), pp. 53–56, doi:10.1145/357980.358001.
  4. Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch & Simon Winwood (2009): seL4: Formal Verification of an OS Kernel. In: 22nd SOSP. ACM, Big Sky, MT, USA, pp. 207–220.
  5. Till Mossakowski, Lutz Schröder & Sergey Goncharov (2008): A Generic Complete Dynamic Logic for Reasoning About Purity and Effects. In: José Fiadeiro & Paola Inverardi: Fundamental Approaches to Software Engineering, Lecture Notes in Computer Science 4961. Springer Berlin / Heidelberg, pp. 199–214, doi:10.1007/978-3-540-78743-3_15.
  6. Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie & Gerwin Klein (2012): Noninterference for Operating System Kernels. In: 2nd Int. Conf. Certified Programs & Proofs. To appear.
  7. Thomas Sewell, Simon Winwood, Peter Gammie, Toby Murray, June Andronick & Gerwin Klein (2011): seL4 Enforces Integrity. In: Marko C. J. D. van Eekelen, Herman Geuvers, Julien Schmaltz & Freek Wiedijk: 2nd ITP, LNCS 6898. Springer-Verlag, Nijmegen, The Netherlands, pp. 325–340, doi:10.1007/978-3-642-22863-6_24.
  8. Christoph Sprenger & David Basin (2007): A Monad-Based Modeling and Verification Toolbox with Application to Security Protocols. In: Klaus Schneider & Jens Brandt: Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science 4732. Springer Berlin / Heidelberg, pp. 302–318, doi:10.1007/978-3-540-74591-4_23.
  9. Wouter Swierstra (2009): A Hoare Logic for the State Monad. In: Stefan Berghofer, Tobias Nipkow, Christian Urban & Makarius Wenzel: Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science 5674. Springer Berlin / Heidelberg, pp. 440–451, doi:10.1007/978-3-642-03359-9_30.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org