swMATH19985MaRDI QIDQ31808FDOQ31808
Author name not available (Why is that?)
Official website: http://compcert.inria.fr/verasco/
Cited In (23)
- MiniLM
- Constructive Galois connections
- A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data
- Refinement to certify abstract interpretations: illustrated on linearization for polyhedra
- Testing your (static analysis) truths
- POPQORN
- Efficient elimination of redundancies in polyhedra by raytracing
- Sparsity preserving algorithms for octagons
- Galculator
- NaCl
- Ctrl
- ARMor
- AUSPICE-R
- Automatically proving termination and memory safety for programs with pointer arithmetic
- AddressSanitizer
- RangeLab
- Verified functional programming of an abstract interpreter
- An abstract memory functor for verified C static analyzers
- SoftBound
- Sound bit-precise numerical domains
- Abstract interpretation as automated deduction
- SafetyKit
- AUSPICE-R: automatic safety-property proofs for realistic features in machine code
This page was built for software: Verasco
