 | 2011 |
|---|
| 11 |       | Sascha Böhme,
Anthony C. J. Fox,
Thomas Sewell,
Tjark Weber:
Reconstruction of Z3's Bit-Vector Proofs in HOL4 and Isabelle/HOL.
CPP 2011: 183-198 |
| 10 | | Anthony C. J. Fox:
LCF-Style Bit-Blasting in HOL4.
ITP 2011: 357-362 |
| 2010 |
|---|
| 9 | | Anthony C. J. Fox,
Magnus O. Myreen:
A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture.
ITP 2010: 243-258 |
| 2009 |
|---|
| 8 | | Jade Alglave,
Anthony C. J. Fox,
Samin Ishtiaq,
Magnus O. Myreen,
Susmit Sarkar,
Peter Sewell,
Francesco Zappa Nardelli:
The semantics of power and ARM multiprocessor machine code.
DAMP 2009: 13-24 |
| 2007 |
|---|
| 7 | | Magnus O. Myreen,
Anthony C. J. Fox,
Michael J. C. Gordon:
Hoare Logic for ARM Machine Code.
FSEN 2007: 272-286 |
| 2005 |
|---|
| 6 | | Anthony C. J. Fox:
An Algebraic Framework for Verifying the Correctness of Hardware with Input and Output: A Formalization in HOL.
CALCO 2005: 157-174 |
| 2003 |
|---|
| 5 | | Anthony C. J. Fox:
Formal Specification and Verification of ARM6.
TPHOLs 2003: 25-40 |
| 4 | | Anthony C. J. Fox,
Neal A. Harman:
Algebraic models of correctness for abstract pipelines.
J. Log. Algebr. Program. 57(1-2): 71-107 (2003) |
| 2000 |
|---|
| 3 | | Anthony C. J. Fox,
Neal A. Harman:
Algebraic Models of Correctness for Microprocessors.
Formal Asp. Comput. 12(4): 298-312 (2000) |
| 1998 |
|---|
| 2 | | Anthony C. J. Fox,
Neal A. Harman:
Algebraic Models of Superscalar Microprocessor Implementations: A Case Study.
Prospects for Hardware Foundations 1998: 138-183 |
| 1996 |
|---|
| 1 | | Anthony C. J. Fox,
Neal A. Harman:
An Algebraic Model of Correctness for Superscalar Microprocessors.
FMCAD 1996: 346-361 |
Data released under the ODC-BY 1.0 license — See also our legal information page