The following pages link to CompCert (Q21716):
Displaying 50 items.
- Automatic generation and validation of instruction encoders and decoders (Q832306) (← links)
- Coinductive big-step operational semantics (Q1012129) (← links)
- Toward compositional verification of interruptible OS kernels and device drivers (Q1663225) (← links)
- A formal C memory model for separation logic (Q1694027) (← links)
- A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data (Q1739908) (← links)
- Software verification with ITPs should use binary code extraction to reduce the TCB (short paper) (Q1791178) (← links)
- Formalization of a polymorphic subtyping algorithm (Q1791209) (← links)
- Foreword to the special focus on formal proofs for mathematics and computer science (Q2018656) (← links)
- An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model (Q2031429) (← links)
- \texttt{slepice}: towards a verified implementation of type theory in type theory (Q2119108) (← links)
- A formal semantics of the GraalVM intermediate representation (Q2147184) (← links)
- Information-flow control on ARM and POWER multicore processors (Q2147697) (← links)
- Formal verification of cP systems using Coq (Q2152300) (← links)
- Translation certification for smart contracts (Q2163161) (← links)
- Theoretical and practical approaches to the denotational semantics for MDESL based on UTP (Q2198135) (← links)
- Predicate extension of symbolic memory graphs for the analysis of memory safety correctness (Q2226974) (← links)
- A self-certifying compilation framework for WebAssembly (Q2234063) (← links)
- Interactive theorem proving. 5th international conference, ITP 2014, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 14--17, 2014. Proceedings (Q2248021) (← links)
- Exploiting pointer analysis in memory models for deductive verification (Q2287078) (← links)
- Mechanically proving determinacy of hierarchical block diagram translations (Q2287118) (← links)
- Verified compilation of floating-point computations (Q2352505) (← links)
- A formally verified compiler back-end (Q2655327) (← links)
- Full Abstraction for Fair Testing in CCS (Q2848947) (← links)
- A First Step in the Design of a Formally Verified Constraint-Based Testing Tool: FocalTest (Q2900178) (← links)
- Synthesis of Distributed Mobile Programs Using Monadic Types in Coq (Q2914742) (← links)
- Mostly Sound Type System Improves a Foundational Program Verifier (Q2938037) (← links)
- Aliasing Restrictions of C11 Formalized in Coq (Q2938039) (← links)
- Certifiably Sound Parallelizing Transformations (Q2938050) (← links)
- Self-certification (Q2942906) (← links)
- (Q3075241) (← links)
- Simple, Functional, Sound and Complete Parsing for All Context-Free Grammars (Q3100206) (← links)
- Practical Tactics for Separation Logic (Q3183539) (← links)
- Trace-Based Coinductive Operational Semantics for While (Q3183540) (← links)
- TRX: A Formally Verified Parser Interpreter (Q3558235) (← links)
- (Q4599196) (← links)
- Separation Logic for Non-local Control Flow and Block Scope Variables (Q4910424) (← links)
- The verified CakeML compiler backend (Q4972072) (← links)
- Trace-Relating Compiler Correctness and Secure Compilation (Q5041085) (← links)
- Practical Proof Search for Coq by Type Inhabitation (Q5048991) (← links)
- Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs (Q5048997) (← links)
- A Fast Verified Liveness Analysis in SSA Form (Q5049011) (← links)
- ANF preserves dependent types up to extensional equality (Q5051989) (← links)
- The Braga Method: Extracting Certified Algorithms from Complex Recursive Schemes in Coq (Q5081874) (← links)
- (Q5119393) (← links)
- A certified framework for compiling and executing garbage-collected languages (Q5176947) (← links)
- (Q5219926) (← links)
- Handcrafted Inversions Made Operational on Operational Semantics (Q5327354) (← links)
- Towards automatic resource bound analysis for OCaml (Q5370874) (← links)
- CompCertTSO (Q5395719) (← links)
- How to make ad hoc proof automation less ad hoc (Q5398327) (← links)
