CompCert
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Practical Tactics for Separation Logic
- Braga Method
- Practical Proof Search for Coq by Type Inhabitation
- Certifiably Sound Parallelizing Transformations
- Trace-relating compiler correctness and secure compilation
- 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
- xJsnark
- Synthesis of distributed mobile programs using monadic types in Coq
- 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 verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data
- A trusted mechanised JavaSript specification
- \texttt{slepice}: towards a verified implementation of type theory in type theory
- scientific article; zbMATH DE number 5850137 (Why is no real title available?)
- TRX: a formally verified parser interpreter
- Simple, functional, sound and complete parsing for all context-free grammars
- How to make ad hoc proof automation less ad hoc
- Foreword to the special focus on formal proofs for mathematics and computer science
- scientific article; zbMATH DE number 7243675 (Why is no real title available?)
- Program logics for certified compilers
- An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model
- Formal verification of cP systems using Coq
- MoSeL
- Verified compilation of floating-point computations
- A formal semantics of the GraalVM intermediate representation
- Information-flow control on ARM and POWER multicore processors
- Individuation criteria, dot-types and copredication: a view from modern type theories
- CoqJVM
- TVOC
- VLISP
- LLVM
- FocalTest
- Euclide
- CompCertTSO
- CakeML
- TRX
- Lem
- ABC
- Cayenne
- cminor
- CVT
- NaCl
- Toolchain
- VeriSmall
- TSOTool
- Ynot
- Mtac
- Vellvm
- TCB
- Verilog
- ARMor
- kPWorkbench
- Pilsner
- SL2SX
- Verasco
- Fiat
- CertiKOS
- RAML
- CertiCoq
- CompCertS
- GCminor
- CSimpl
- MLCompCert
- UTPCalc
- TIL
- Rocksalt
- PureScript
- Diablo
- Bedrock
- Template-Coq
- Piton
- VST-Floyd
- C-to-Isabelle
- TALx86
- GraalVM
- FreeSpec
- ADSafe
- TSL
- MetaCoq
- Crellvm
- Loopy
- WebAssembly
- 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
- Toward compositional verification of interruptible OS kernels and device drivers
- Predicate extension of symbolic memory graphs for the analysis of memory safety correctness
- Full abstraction for fair testing in CCS
- Translation certification for smart contracts
- Formalization of a polymorphic subtyping algorithm
This page was built for software: CompCert
