References

1. Gertrud Bauer & Markus Wenzel (2001): Calculational Reasoning Revisited – An Isabelle/Isar experience. In: 14th TPHOLs. Springer-Verlag, pp. 75–90, doi:10.1007/3-540-44755-5_7.
2. Orieta Celiku & Annabelle McIver (2004): Cost-based analysis of probabilistic programs mechanised in HOL. Nordic J. of Computing 11(2), pp. 102–128. Available at http://www.cse.unsw.edu.au/~carrollm/probs/Papers/ Celiku-04.pdf.
3. David Cock (2011): Exploitation as an inference problem. In: 4th AISEC, Chicago, IL, USA, pp. 105–106, doi:10.1145/2046684.2046702.
4. 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, doi:10.1007/978-3-540-71067-7_16.
5. Edsger W. Dijkstra (1975): Guarded commands, nondeterminacy and formal derivation of programs. CACM 18(8), pp. 453–457, doi:10.1145/360933.360975.
6. Joseph Goguen & José Meseguer (1982): Security Policies and Security Models. In: IEEE Symp. Security & Privacy. Comp. Soc., Oakland, California, USA, pp. 11–20.
7. William L. Harrison & Richard B. Kieburtz (2005): The logic of demand in Haskell. J. Functional Progr. 15(6), pp. 837–891, doi:10.1017/S0956796805005666.
8. Joe Hurd, Annabelle McIver & Carroll Morgan (2005): Probabilistic guarded commands mechanized in HOL. Theoretical Computer Science 346(1), pp. 96 – 112, doi:10.1016/j.tcs.2005.08.005. Available at http://www.sciencedirect.com/science/article/pii/ S0304397505004767.
9. 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, doi:10.1145/1629575.1629596.
10. Annabelle McIver & Carroll Morgan (2001): Partial correctness for probabilistic demonic programs. Theoretical Comp. Sci. 266(12), pp. 513 – 541, doi:10.1016/S0304-3975(00)00208-5. Available at http://www.sciencedirect.com/science/article/pii/ S0304397500002085.
11. Annabelle McIver & Carroll Morgan (2004): Abstraction, Refinement and Proof for Probabilistic Systems. Springer.
12. Till Mossakowski, Lutz Schröder & Sergey Goncharov (2010): A generic complete dynamic logic for reasoning about purity and effects. Formal Aspects Comput. 22(3-4), pp. 363–384, doi:10.1007/s00165-010-0153-4.
13. Tobias Nipkow (2002): Hoare Logics in Isabelle/HOL. In: H. Schwichtenberg & R. Steinbrüggen: Proof and System-Reliability. Kluwer, pp. 341–367.
14. Tobias Nipkow, Lawrence Paulson & Markus Wenzel (2002): Isabelle/HOL — A Proof Assistant for Higher-Order Logic. LNCS 2283. Springer-Verlag.
15. Steve Selvin (1975): A problem in probability (letter to the editor). American Statistician 29(1), pp. 67.

Comments and questions to: eptcs@eptcs.org

For website issues: webmaster@eptcs.org