An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model (Q2031429): Difference between revisions

@@ Property / cites work @@
+Fences in weak memory models
@@ Property / cites work: Fences in weak memory models / rank @@
+Normal rank
@@ Property / cites work @@
+Formalising Java’s Data Race Free Guarantee
@@ Property / cites work: Formalising Java’s Data Race Free Guarantee / rank @@
+Normal rank
@@ Property / cites work @@
+CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types
+Normal rank
@@ Property / cites work @@
+Relaxed memory models
@@ Property / cites work: Relaxed memory models / rank @@
+Normal rank
@@ Property / cites work @@
+Effective Program Verification for Relaxed Memory Models
+Normal rank
@@ Property / cites work @@
+Secure Microkernels, State Monads and Scalable Refinement
+Normal rank
@@ Property / cites work @@
+A Calculus for Relaxed Memory
@@ Property / cites work: A Calculus for Relaxed Memory / rank @@
+Normal rank
@@ Property / cites work @@
+Improved Tool Support for Machine-Code Decompilation in HOL4
+Normal rank
@@ Property / cites work @@
+A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture
+Normal rank
@@ Property / cites work @@
+Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties
+Normal rank
@@ Property / cites work @@
+Formal certification of a compiler back-end or
@@ Property / cites work: Formal certification of a compiler back-end or / rank @@
+Normal rank
@@ Property / cites work @@
+Lem
@@ Property / cites work: Lem / rank @@
+Normal rank
@@ Property / cites work @@
+An overview of the K semantic framework
@@ Property / cites work: An overview of the K semantic framework / rank @@
+Normal rank
@@ Property / cites work @@
+Towards a Unified Theory of Operational and Axiomatic Semantics
+Normal rank