CompCert

swMATH9737MaRDI QIDQ21716FDOQ21716

Author name not available (Why is that?)

Described by source

• CompCertS: a memory-aware verified C compiler using pointer as integer semantics
• Compositional CompCert

Cited In (53)

• Mechanically proving determinacy of hierarchical block diagram translations
• Coinductive big-step operational semantics
• Aliasing Restrictions of C11 Formalized in Coq
• Automatic generation and validation of instruction encoders and decoders
• Title not available (Why is that?)
• A self-certifying compilation framework for WebAssembly
• A formally verified compiler back-end
• A First Step in the Design of a Formally Verified Constraint-Based Testing Tool: FocalTest
• A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data
• \texttt{slepice}: towards a verified implementation of type theory in type theory
• Synthesis of Distributed Mobile Programs Using Monadic Types in Coq
• Title not available (Why is that?)
• Title not available (Why is that?)
• How to make ad hoc proof automation less ad hoc
• Title not available (Why is that?)
• Foreword to the special focus on formal proofs for mathematics and computer science
• Mostly Sound Type System Improves a Foundational Program Verifier
• Trace-Relating Compiler Correctness and Secure Compilation
• An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model
• Self-certification
• Formal verification of cP systems using Coq
• Verified compilation of floating-point computations
• Separation Logic for Non-local Control Flow and Block Scope Variables
• A formal semantics of the GraalVM intermediate representation
• Information-flow control on ARM and POWER multicore processors
• An operational and axiomatic semantics for non-determinism and sequence points in C
• The Braga Method: Extracting Certified Algorithms from Complex Recursive Schemes in Coq
• Theoretical and practical approaches to the denotational semantics for MDESL based on UTP
• Predicate extension of symbolic memory graphs for the analysis of memory safety correctness
• Toward compositional verification of interruptible OS kernels and device drivers
• Handcrafted Inversions Made Operational on Operational Semantics
• Translation certification for smart contracts
• Simple, Functional, Sound and Complete Parsing for All Context-Free Grammars
• CompCertTSO
• Formalization of a polymorphic subtyping algorithm
• Software verification with ITPs should use binary code extraction to reduce the TCB (short paper)
• The verified CakeML compiler backend
• A certified framework for compiling and executing garbage-collected languages
• TRX: A Formally Verified Parser Interpreter
• Exploiting pointer analysis in memory models for deductive verification
• 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
• Trace-Based Coinductive Operational Semantics for While
• A Fast Verified Liveness Analysis in SSA Form
• Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs
• ANF preserves dependent types up to extensional equality
• Practical Tactics for Separation Logic
• Practical Proof Search for Coq by Type Inhabitation
• Certifiably Sound Parallelizing Transformations
• Full Abstraction for Fair Testing in CCS
• A formal C memory model for separation logic
• A trusted mechanised JavaScript specification
• Towards automatic resource bound analysis for OCaml
• Program Logics for Certified Compilers

This page was built for software: CompCert