CompCert
From MaRDI portal
Software:21716
swMATH9737MaRDI QIDQ21716FDOQ21716
Author name not available (Why is that?)
Cited In (53)
- Mechanically proving determinacy of hierarchical block diagram translations
- Coinductive big-step operational semantics
- Automatic generation and validation of instruction encoders and decoders
- Mostly sound type system improves a foundational program verifier
- A self-certifying compilation framework for WebAssembly
- A formally verified compiler back-end
- Self-certification: bootstrapping certified typecheckers in F\(^\ast\) with Coq
- A trusted mechanised JavaSript specification
- 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
- Title not available (Why is that?)
- TRX: a formally verified parser interpreter
- How to make ad hoc proof automation less ad hoc
- Simple, functional, sound and complete parsing for all context-free grammars
- Program logics for certified compilers
- Title not available (Why is that?)
- Foreword to the special focus on formal proofs for mathematics and computer science
- An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model
- Formal verification of cP systems using Coq
- Verified compilation of floating-point computations
- Individuation criteria, dot-types and copredication: a view from modern type theories
- 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
- Full abstraction for fair testing in CCS
- Translation certification for smart contracts
- 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
- Interactive theorem proving from the perspective of Isabelle/Isar
- 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
- Trace-relating compiler correctness and secure compilation
- Certifiably Sound Parallelizing Transformations
- Aliasing restrictions of C11 formalized in Coq
- A formal C memory model for separation logic
- Separation logic for non-local control flow and block scope variables
- Handcrafted inversions made operational on operational semantics
- Towards automatic resource bound analysis for OCaml
- A first step in the design of a formally verified constraint-based testing tool: FocalTest
- Synthesis of distributed mobile programs using monadic types in Coq
This page was built for software: CompCert
