CompCertS: a memory-aware verified C compiler using pointer as integer semantics (Q1687720): Difference between revisions

@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+CompCertTSO
@@ Property / describes a project that uses: CompCertTSO / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W2746152268
@@ Property / OpenAlex ID: W2746152268 / 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 @@
+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 @@
+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:1687720