swMATH9737MaRDI QIDQ21716FDOQ21716
Author name not available (Why is that?)
Official website: http://compcert.inria.fr/
Cited In (only showing first 100 items - show all)
- COMPCERTSFI
- Mostly sound type system improves a foundational program verifier
- Self-certification: bootstrapping certified typecheckers in F\(^\ast\) with Coq
- \texttt{slepice}: towards a verified implementation of type theory in type theory
- Title not available (Why is that?)
- MoSeL
- 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
- 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
- Translation certification for smart contracts
- Exploiting pointer analysis in memory models for deductive verification
- 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
- Trace-relating compiler correctness and secure compilation
- 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
- A self-certifying compilation framework for WebAssembly
- A formally verified compiler back-end
- A trusted mechanised JavaSript specification
- A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data
- 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
- 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
- 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
- Toward compositional verification of interruptible OS kernels and device drivers
- Full abstraction for fair testing in CCS
- LLVM
- FocalTest
- Euclide
- CompCertTSO
- CakeML
- TRX
- Lem
- ABC
- Cayenne
- cminor
- CVT
- NaCl
- Toolchain
- VeriSmall
- TSOTool
- Ynot
- Mtac
- Vellvm
- TCB
- Verilog
- 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
- 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
- A certified framework for compiling and executing garbage-collected languages
- Interactive theorem proving from the perspective of Isabelle/Isar
- GraalVM
- FreeSpec
- ADSafe
- TSL
- MetaCoq
- Crellvm
- Loopy
- 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
- Trace-Based Coinductive Operational Semantics for While
- PaSAT
This page was built for software: CompCert
