An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model

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

zbMATH Keywords

Isabelle/HOLweak memory modelform verificationinstruction set architectureTSO

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• ACL2
• Isabelle/HOL
• CoqJVM
• Lem
• CompCert
• TSOTool
• K Prover
• TSL

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