Output details
11 - Computer Science and Informatics
University of Cambridge
Output title
A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture
Type
E - Conference contribution
Name of conference/published proceedings
INTERACTIVE THEOREM PROVING, PROCEEDINGS
Volume number
6172
Issue number
-
First page of article
243
ISSN of proceedings
0302-9743
Year of publication
2010
URL
-
Number of additional authors
1
Additional information
<07> This is ground-breaking work in developing highly detailed instruction set models and associated theorem proving tools, which are used to reason about low-level code, and it contributes both to safety-critical software verification and system-level security analysis. The ARM architecture is of enormous interest, because billions of ARM-based processors have been manufactured. Our models and tools have been used by various academic and commercial groups throughout the world; most significantly, our ARM model is being used in the seL4 verified micro-kernel project at NICTA. http://ssrg.nicta.com.au/projects/seL4/
Interdisciplinary
-
Cross-referral requested
-
Research group
None
Citation count
14
Proposed double-weighted
No
Double-weighted statement
-
Reserve for a double-weighted output
No
Non-English
No
English abstract
-
