An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model
From MaRDI portal
Publication:2031429
DOI10.1007/s10817-020-09579-4OpenAlexW3049189160MaRDI QIDQ2031429
Alwen Tiu, Zhé Hóu, Koh Chuen Hoa, David Sanán, Yang Liu, Jin-Song Dong
Publication date: 9 June 2021
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: http://hdl.handle.net/10072/396682
Uses Software
Cites Work
- Fences in weak memory models
- An overview of the K semantic framework
- Lem
- A Calculus for Relaxed Memory
- Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties
- Improved Tool Support for Machine-Code Decompilation in HOL4
- Towards a Unified Theory of Operational and Axiomatic Semantics
- CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types
- Effective Program Verification for Relaxed Memory Models
- Formalising Java’s Data Race Free Guarantee
- Secure Microkernels, State Monads and Scalable Refinement
- Relaxed memory models
- Formal certification of a compiler back-end or
- A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture
This page was built for publication: An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model