Cited in
(only showing first 100 items - show all)- Trace-Based Coinductive Operational Semantics for While
- Coinductive big-step operational semantics
- The verified CakeML compiler backend
- Separation logic for non-local control flow and block scope variables
- An operational and axiomatic semantics for non-determinism and sequence points in C
- Handcrafted inversions made operational on operational semantics
- A self-certifying compilation framework for WebAssembly
- Toward compositional verification of interruptible OS kernels and device drivers
- A formal C memory model for separation logic
- Automatic generation and validation of instruction encoders and decoders
- Practical Proof Search for Coq by Type Inhabitation
- Interactive theorem proving from the perspective of Isabelle/Isar
- The Braga Method: Extracting Certified Algorithms from Complex Recursive Schemes in Coq
- A formally verified compiler back-end
- CompCertTSO
- An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model
- Verified compilation of floating-point computations
- Aliasing restrictions of C11 formalized in Coq
- Full abstraction for fair testing in CCS
- A first step in the design of a formally verified constraint-based testing tool: FocalTest
- scientific article; zbMATH DE number 5850137 (Why is no real title available?)
- A trusted mechanised JavaSript specification
- A certified framework for compiling and executing garbage-collected languages
- CoqJVM
- TVOC
- VLISP
- LLVM
- FocalTest
- Euclide
- CompCertTSO
- CakeML
- TRX
- Lem
- ABC
- Cayenne
- cminor
- CVT
- NaCl
- Toolchain
- VeriSmall
- TSOTool
- Ynot
- Mtac
- Vellvm
- TCB
- Verilog
- Towards automatic resource bound analysis for OCaml
- 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
- TRX: a formally verified parser interpreter
- GraalVM
- FreeSpec
- ADSafe
- TSL
- MetaCoq
- Crellvm
- Loopy
- WebAssembly
- Program logics for certified compilers
- PaSAT
- Braga Method
- How to make ad hoc proof automation less ad hoc
- Foreword to the special focus on formal proofs for mathematics and computer science
- Simple, functional, sound and complete parsing for all context-free grammars
- Formalization of a polymorphic subtyping algorithm
- Software verification with ITPs should use binary code extraction to reduce the TCB (short paper)
- A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data
- 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
- Formal verification of cP systems using Coq
- Certifiably Sound Parallelizing Transformations
- COMPCERTSFI
- Practical Tactics for Separation Logic
- Predicate extension of symbolic memory graphs for the analysis of memory safety correctness
- Translation certification for smart contracts
- Self-certification: bootstrapping certified typecheckers in F\(^\ast\) with Coq
- 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
This page was built for software: CompCert
