CompCert
From MaRDI portal
Software:21716
No author found.
Related Items (53)
Trace-Relating Compiler Correctness and Secure Compilation ⋮ Automatic generation and validation of instruction encoders and decoders ⋮ 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 ⋮ A First Step in the Design of a Formally Verified Constraint-Based Testing Tool: FocalTest ⋮ ANF preserves dependent types up to extensional equality ⋮ A formal semantics of the GraalVM intermediate representation ⋮ Information-flow control on ARM and POWER multicore processors ⋮ Practical Tactics for Separation Logic ⋮ Trace-Based Coinductive Operational Semantics for While ⋮ Synthesis of Distributed Mobile Programs Using Monadic Types in Coq ⋮ Formal verification of cP systems using Coq ⋮ Unnamed Item ⋮ Translation certification for smart contracts ⋮ A formally verified compiler back-end ⋮ Toward compositional verification of interruptible OS kernels and device drivers ⋮ The Braga Method: Extracting Certified Algorithms from Complex Recursive Schemes in Coq ⋮ Handcrafted Inversions Made Operational on Operational Semantics ⋮ Mostly Sound Type System Improves a Foundational Program Verifier ⋮ Aliasing Restrictions of C11 Formalized in Coq ⋮ Certifiably Sound Parallelizing Transformations ⋮ Self-certification ⋮ A formal C memory model for separation logic ⋮ Theoretical and practical approaches to the denotational semantics for MDESL based on UTP ⋮ Towards automatic resource bound analysis for OCaml ⋮ Unnamed Item ⋮ Predicate extension of symbolic memory graphs for the analysis of memory safety correctness ⋮ How to make ad hoc proof automation less ad hoc ⋮ A self-certifying compilation framework for WebAssembly ⋮ A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data ⋮ TRX: A Formally Verified Parser Interpreter ⋮ A trusted mechanised JavaScript specification ⋮ An operational and axiomatic semantics for non-determinism and sequence points in C ⋮ Separation Logic for Non-local Control Flow and Block Scope Variables ⋮ 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 ⋮ A certified framework for compiling and executing garbage-collected languages ⋮ 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 ⋮ Software verification with ITPs should use binary code extraction to reduce the TCB (short paper) ⋮ Formalization of a polymorphic subtyping algorithm ⋮ Exploiting pointer analysis in memory models for deductive verification ⋮ Mechanically proving determinacy of hierarchical block diagram translations ⋮ Coinductive big-step operational semantics ⋮ Unnamed Item ⋮ The verified CakeML compiler backend ⋮ Unnamed Item ⋮ Simple, Functional, Sound and Complete Parsing for All Context-Free Grammars ⋮ CompCertTSO ⋮ Program Logics for Certified Compilers ⋮ Full Abstraction for Fair Testing in CCS ⋮ Verified compilation of floating-point computations ⋮ \texttt{slepice}: towards a verified implementation of type theory in type theory
This page was built for software: CompCert
