forked from acjf3/acjf3.github.io
-
Notifications
You must be signed in to change notification settings - Fork 0
/
publications.html
46 lines (39 loc) · 4.46 KB
/
publications.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
<html>
<head><title>Publications: Anthony Fox</title>
<link rel="stylesheet" href="screen.css" type="text/css" media="screen" >
<link rel="stylesheet" href="mobile.css" type="text/css" media="only screen and (max-device-width: 480px)" >
</head>
<body>
<h1><a href="index.html">Anthony Fox</a></h1>
<h2>Publications and reports</h2>
<ul>
<li>Anthony Fox, Magnus O. Myreen, Yong Kiam Tan, Ramana Kumar. <a href="papers/cpp17.pdf">Verified Compilation of CakeML to Multiple Machine-Code Targets</a>. CPP'17, 2017.</li>
<li>Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony Fox, Scott Owens and Michael Norrish. <a href="papers/icfp16main-main43-p-1febe15-27947-preprint.pdf">A New Verified Compiler Backend for CakeML</a>. ICFP'16, 2016.</li>
<li>Anthony Fox. <a href="papers/itp15.pdf">Improved Tool Support for Machine-Code Decompilation in HOL4</a>. In Interactive Theorem Proving (ITP), 2015.</li>
<li>Anthony Fox. <a href="papers/itp12.pdf">Directions in ISA specification</a>. In Interactive Theorem Proving (ITP), 2012.</li>
<li>Sascha Böhme, Anthony Fox, Thomas Sewell and Tjark Weber. Reconstruction of Z3's Bit-Vector Proofs in HOL4 and Isabelle/HOL. In First International Conference on Certified Programs and Proofs (CPP 2011).</li>
<li>Anthony Fox. <a class="apaper" href="http://www.cl.cam.ac.uk/%7Eacjf3/papers/blast.pdf">LCF-style Bit-Blasting in HOL4</a>. In Interactive Theorem Proving (ITP), 2011.</li>
<li>Anthony Fox and Magnus O. Myreen. <a class="apaper" href="http://www.cl.cam.ac.uk/%7Emom22/itp10-armv7.pdf">A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture</a>. In Interactive Theorem Proving (ITP), 2010.</li>
<li>Anthony Fox, Michael Gordon, and Magnus O. Myreen. <a href="papers/08Gordon.pdf">Specification and verification of ARM hardware and software</a>. In David S. Hardin, editor, <span style="font-style: italic;">Design and Verification of Microprocessor Systems for High-Assurance Applications</span>, pages 221-248. Springer, 2010.</li>
<li>Jade Alglave, Anthony Fox, Samin Ishtiaq, Magnus O. Myreen, Susmit Sarkar, Peter Sewell, and Francesco Zappa Nardelli. <a href="http://doi.acm.org/10.1145/1481839.1481842">The Semantics of Power and ARM Multiprocessor Machine Code</a>. DAMP 09.</li>
<li>Magnus O. Myreen, Anthony Fox and Michael Gordon. <a href="http://www.cl.cam.ac.uk/%7Emom22/arm-hoare-logic.pdf">Hoare Logic for ARM Machine Code</a>. In Fundamentals of Software Engineering (FSEN), 2007.</li>
<li>Anthony Fox. An algebraic framework for verifying the correctness of hardware with input and output: a formalization in HOL. In J.L. Fiadeiro et al. (Eds.): CALCO 2005, LNCS 3629, pp. 157-174, 2005.</li>
<li>Anthony Fox and Neal Harman. Algebraic models of correctness for abstract pipelines. The Journal of Logic and Algebraic Programming, 57(1-2): 71-107, 2003.
<li>Anthony Fox. Formal specification and verification of ARM6. In David Basin and Burkhart Wolff, editors, TPHOLs '03, volume 2758 of LNCS, pages 25-40. Springer-Verlag, 2003.
<li>Anthony Fox. <a href="http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-548.html">Formal verification of the ARM6 micro-architecture</a>. Technical report No. 548, University of Cambridge Computer Laboratory, November 2002. </li>
<li>Anthony Fox. <a href="http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-545.html">A HOL specification of the ARM instruction set architecture</a>. Technical report No. 545, University of Cambridge Computer Laboratory, June 2001. </li>
<li>Anthony Fox. <a href="http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-512.html">An algebraic framework for modelling and verifying microprocessors using HOL</a>. Technical report No. 512, University of Cambridge Computer Laboratory, April 2001. </li>
<li>Anthony Fox and Neal Harman. Algebraic Models of Correctness for Microprocessors. <i>Formal Aspects of Computing</i>, 12(4): 298-312, 2000. </li>
<li>Anthony Fox. Algebraic Models for Advanced Microprocessors, PhD thesis, Swansea University, 1998. </li>
<li>Anthony Fox and Neal Harman. Algebraic Models of Superscalar Microprocessor Implementations: A Case Study. Prospects for Hardware Foundations: 138-183, 1998.
<li>Anthony Fox and Neal Harman. An Algebraic Model of Correctness for Superscalar Microprocessors. FMCAD: 346-361, 1996.</li>
</li>
</ul>
<h2>Other papers</h2>
<ul>
<li><a href="papers/bdt.pdf">Verifying the ARM Block Data Transfer Instructions.</a> <i>Presented at DCC 2004.</i> </li>
<li><a href="papers/mul.pdf">Verifying ARM6 Multiplication.</a></li>
</ul>
<p> </p>
</body>
</html>