A formally verified compiler back-end (Q2655327): Difference between revisions

@@ Property / describes a project that uses @@
+CompCert
@@ Property / describes a project that uses: CompCert / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W2148662736
@@ Property / OpenAlex ID: W2148662736 / rank @@
+Normal rank
@@ Property / Wikidata QID @@
+Q123335679
@@ Property / Wikidata QID: Q123335679 / rank @@
+Normal rank
@@ Property / arXiv ID @@
+.2137
@@ Property / arXiv ID: 0902.2137 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4343027
@@ Property / cites work: Q4343027 / rank @@
+Normal rank
@@ Property / cites work @@
+Separation Logic for Small-Step cminor
@@ Property / cites work: Separation Logic for Small-Step cminor / rank @@
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
+Normal rank
@@ Property / cites work @@
+Certificate Translation for Optimizing Compilers
@@ Property / cites work: Certificate Translation for Optimizing Compilers / rank @@
+Normal rank
@@ Property / cites work @@
+Certificate Translation in Abstract Interpretation
+Normal rank
@@ Property / cites work @@
+Biorthogonality, step-indexing and compiler correctness
+Normal rank
@@ Property / cites work @@
+Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
+Normal rank
@@ Property / cites work @@
+Types for Proofs and Programs
@@ Property / cites work: Types for Proofs and Programs / rank @@
+Normal rank
@@ Property / cites work @@
+Mechanized semantics for the clight subset of the C language
+Normal rank
@@ Property / cites work @@
+Extracting a data flow analyser in constructive logic
+Normal rank
@@ Property / cites work @@
+Toward compiler implementation correctness proofs
@@ Property / cites work: Toward compiler implementation correctness proofs / rank @@
+Normal rank
@@ Property / cites work @@
+Types for Proofs and Programs
@@ Property / cites work: Types for Proofs and Programs / rank @@
+Normal rank
@@ Property / cites work @@
+Q4474214
@@ Property / cites work: Q4474214 / rank @@
+Normal rank
@@ Property / cites work @@
+Static Analysis
@@ Property / cites work: Static Analysis / rank @@
+Normal rank
@@ Property / cites work @@
+Q5302558
@@ Property / cites work: Q5302558 / 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 @@
+The Zipper
@@ Property / cites work: The Zipper / rank @@
+Normal rank
@@ Property / cites work @@
+Q4068060
@@ Property / cites work: Q4068060 / rank @@
+Normal rank
@@ Property / cites work @@
+Proving correctness of compiler optimizations by temporal logic
+Normal rank
@@ Property / cites work @@
+Automated soundness proofs for dataflow analyses and transformations via local rules
+Normal rank
@@ Property / cites work @@
+Java bytecode verification: Algorithms and formalizations
+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 @@
+Coinductive big-step operational semantics
@@ Property / cites work: Coinductive big-step operational semantics / rank @@
+Normal rank
@@ Property / cites work @@
+Q4435471
@@ Property / cites work: Q4435471 / rank @@
+Normal rank
@@ Property / cites work @@
+Extraction in Coq: An Overview
@@ Property / cites work: Extraction in Coq: An Overview / rank @@
+Normal rank
@@ Property / cites work @@
+Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic
+Normal rank
@@ Property / cites work @@
+Compilation as Rewriting in Higher Order Logic
@@ Property / cites work: Compilation as Rewriting in Higher Order Logic / rank @@
+Normal rank
@@ Property / cites work @@
+Q5574395
@@ Property / cites work: Q5574395 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5674962
@@ Property / cites work: Q5674962 / rank @@
+Normal rank
@@ Property / cites work @@
+Stack-based typed assembly language
@@ Property / cites work: Stack-based typed assembly language / rank @@
+Normal rank
@@ Property / cites work @@
+Stack-based typed assembly language
@@ Property / cites work: Stack-based typed assembly language / rank @@
+Normal rank
@@ Property / cites work @@
+Modular compiler verification. A refinement-algebraic approach advocating stepwise abstraction
+Normal rank
@@ Property / cites work @@
+Q4738390
@@ Property / cites work: Q4738390 / rank @@
+Normal rank
@@ Property / cites work @@
+Oracle-based checking of untrusted software
@@ Property / cites work: Oracle-based checking of untrusted software / rank @@
+Normal rank
@@ Property / cites work @@
+Resources, concurrency, and local reasoning
@@ Property / cites work: Resources, concurrency, and local reasoning / rank @@
+Normal rank
@@ Property / cites work @@
+Tilting at windmills with Coq: Formal verification of a compilation algorithm for parallel moves
+Normal rank
@@ Property / cites work @@
+Symbolic transfer function-based approaches to certified compilation
+Normal rank
@@ Property / cites work @@
+Q2742791
@@ Property / cites work: Q2742791 / rank @@
+Normal rank
@@ Property / cites work @@
+Formal verification of translation validators
@@ Property / cites work: Formal verification of translation validators / rank @@
+Normal rank