\textsc{CompCertS}: a memory-aware verified C compiler using a pointer as integer semantics (Q2319992): Difference between revisions

@@ Property / describes a project that uses @@
+CompCertTSO
@@ Property / describes a project that uses: CompCertTSO / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+CompCertS
@@ Property / describes a project that uses: CompCertS / 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/s10817-018-9496-y
+Normal rank
@@ Property / OpenAlex ID @@
+W2901282687
@@ Property / OpenAlex ID: W2901282687 / rank @@
+Normal rank
@@ Property / Wikidata QID @@
+Q122874428
@@ Property / Wikidata QID: Q122874428 / rank @@
+Normal rank
@@ Property / cites work @@
+A Concrete Memory Model for CompCert
@@ Property / cites work: A Concrete Memory Model for CompCert / rank @@
+Normal rank
@@ Property / cites work @@
+A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data
+Normal rank
@@ Property / cites work @@
+Aliasing Restrictions of C11 Formalized in Coq
@@ Property / cites work: Aliasing Restrictions of C11 Formalized in Coq / rank @@
+Normal rank
@@ Property / cites work @@
+An operational and axiomatic semantics for non-determinism and sequence points in C
+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 @@
+A Formally-Verified Alias Analysis
@@ Property / cites work: A Formally-Verified Alias Analysis / rank @@
+Normal rank
@@ Property / cites work @@
+CompCertTSO
@@ Property / cites work: CompCertTSO / rank @@
+Normal rank
@@ links / mardi / name / links / mardi / name @@
+Publication:2319992