CompCert
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Coinductive big-step operational semantics
- Braga Method
- CoqJVM
- TVOC
- VLISP
- Toward compositional verification of interruptible OS kernels and device drivers
- A formal C memory model for separation logic
- LLVM
- A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data
- Software verification with ITPs should use binary code extraction to reduce the TCB (short paper)
- Formalization of a polymorphic subtyping algorithm
- FocalTest
- Euclide
- Foreword to the special focus on formal proofs for mathematics and computer science
- CompCertTSO
- An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model
- CakeML
- TRX
- \texttt{slepice}: towards a verified implementation of type theory in type theory
- Lem
- A formal semantics of the GraalVM intermediate representation
- Information-flow control on ARM and POWER multicore processors
- Toolchain
- Formal verification of cP systems using Coq
- Translation certification for smart contracts
- Cayenne
- ABC
- cminor
- VeriSmall
- NaCl
- CVT
- Theoretical and practical approaches to the denotational semantics for MDESL based on UTP
- TSOTool
- Predicate extension of symbolic memory graphs for the analysis of memory safety correctness
- A self-certifying compilation framework for WebAssembly
- 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
- Exploiting pointer analysis in memory models for deductive verification
- Mechanically proving determinacy of hierarchical block diagram translations
- Verified compilation of floating-point computations
- Ynot
- Mtac
- Vellvm
- TCB
- Verilog
- A formally verified compiler back-end
- Full abstraction for fair testing in CCS
- 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
- Mostly sound type system improves a foundational program verifier
- Aliasing restrictions of C11 formalized in Coq
- Certifiably Sound Parallelizing Transformations
- Self-certification: bootstrapping certified typecheckers in F^ with Coq
- ARMor
- scientific article; zbMATH DE number 5850137 (Why is no real title available?)
- Simple, functional, sound and complete parsing for all context-free grammars
- kPWorkbench
- Verasco
- Pilsner
- Practical Tactics for Separation Logic
- Trace-Based Coinductive Operational Semantics for While
- SL2SX
- Fiat
- CertiKOS
- RAML
- UTPCalc
- TIL
- GCminor
- MLCompCert
- CompCertS
- CSimpl
- CertiCoq
- Rocksalt
- TRX: a formally verified parser interpreter
- PureScript
- Diablo
- Template-Coq
- VST-Floyd
- Bedrock
- Piton
- C-to-Isabelle
- Individuation criteria, dot-types and copredication: a view from modern type theories
- TALx86
- Separation logic for non-local control flow and block scope variables
- The verified CakeML compiler backend
- Trace-relating compiler correctness and secure compilation
- Practical Proof Search for Coq by Type Inhabitation
- Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs
- A Fast Verified Liveness Analysis in SSA Form
- ANF preserves dependent types up to extensional equality
- The Braga Method: Extracting Certified Algorithms from Complex Recursive Schemes in Coq
- Compiling with classical connectives
- GraalVM
- A certified framework for compiling and executing garbage-collected languages
- Interactive theorem proving from the perspective of Isabelle/Isar
- FreeSpec
- Handcrafted inversions made operational on operational semantics
- ADSafe
- Towards automatic resource bound analysis for OCaml
- CompCertTSO
- How to make ad hoc proof automation less ad hoc
This page was built for software: CompCert
