Verified Software Toolchain (Q3000569): Difference between revisions

@@ Property / describes a project that uses @@
+Toolchain
@@ Property / describes a project that uses: Toolchain / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+TCB
@@ Property / describes a project that uses: TCB / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/978-3-642-19718-5_1
+Normal rank
@@ Property / OpenAlex ID @@
+W2213989452
@@ Property / OpenAlex ID: W2213989452 / rank @@
+Normal rank
@@ Property / cites work @@
+A very modal model of a modern, major, general type system
+Normal rank
@@ Property / cites work @@
+A trustworthy proof checker
@@ Property / cites work: A trustworthy proof checker / rank @@
+Normal rank
@@ Property / cites work @@
+Step-indexed kripke models over recursive worlds
@@ Property / cites work: Step-indexed kripke models over recursive worlds / rank @@
+Normal rank
@@ Property / cites work @@
+Permission accounting in separation logic
@@ Property / cites work: Permission accounting in separation logic / rank @@
+Normal rank
@@ Property / cites work @@
+Relaxed memory models
@@ Property / cites work: Relaxed memory models / rank @@
+Normal rank
@@ Property / cites work @@
+Foundational certified code in the Twelf metalogical framework
+Normal rank
@@ Property / cites work @@
+Local Reasoning for Storable Locks and Threads
@@ Property / cites work: Local Reasoning for Storable Locks and Threads / rank @@
+Normal rank
@@ Property / cites work @@
+Oracle Semantics for Concurrent Separation Logic
@@ Property / cites work: Oracle Semantics for Concurrent Separation Logic / rank @@
+Normal rank
@@ Property / cites work @@
+A theory of indirection via approximation
@@ Property / cites work: A theory of indirection via approximation / rank @@
+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 @@
+Formal verification of a C-like memory model and its uses for verifying program transformations
+Normal rank
@@ Property / cites work @@
+Resources, concurrency, and local reasoning
@@ Property / cites work: Resources, concurrency, and local reasoning / rank @@
+Normal rank
@@ Property / cites work @@
+Logic for Programming, Artificial Intelligence, and Reasoning
+Normal rank