Formal reasoning under cached address translation (Q2209539): Difference between revisions

@@ Property / full work available at URL @@
+https://doi.org/10.1007/s10817-019-09539-7
+Normal rank
@@ Property / OpenAlex ID @@
+W2999427823
@@ Property / OpenAlex ID: W2999427823 / rank @@
+Normal rank
@@ Property / cites work @@
+Physical addressing on real hardware in Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+Concerned with the unprivileged: user programs in kernel refinement
+Normal rank
@@ Property / cites work @@
+A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture
+Normal rank
@@ Property / cites work @@
+Deep Specifications and Certified Abstraction Layers
+Normal rank
@@ Property / cites work @@
+Types, Maps and Separation Logic
@@ Property / cites work: Types, Maps and Separation Logic / rank @@
+Normal rank
@@ Property / cites work @@
+Q4247084
@@ Property / cites work: Q4247084 / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+A Brief Overview of HOL4
@@ Property / cites work: A Brief Overview of HOL4 / rank @@
+Normal rank
@@ Property / cites work @@
+Reasoning about Translation Lookaside Buffers
@@ Property / cites work: Reasoning about Translation Lookaside Buffers / rank @@
+Normal rank
@@ Property / cites work @@
+Program verification in the presence of cached address translation
+Normal rank
@@ Property / Wikidata QID @@
+Q126318699
@@ Property / Wikidata QID: Q126318699 / rank @@
+Normal rank