Cited in
(23)- 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
- Efficient elimination of redundancies in polyhedra by raytracing
- Sparsity preserving algorithms for octagons
- Galculator
- NaCl
- Ctrl
- ARMor
- AUSPICE-R
- AddressSanitizer
- RangeLab
- SafetyKit
- Automatically proving termination and memory safety for programs with pointer arithmetic
- POPQORN
- MiniLM
- Verified functional programming of an abstract interpreter
- An abstract memory functor for verified C static analyzers
- Sound bit-precise numerical domains
- Abstract interpretation as automated deduction
- AUSPICE-R: automatic safety-property proofs for realistic features in machine code
- SoftBound
This page was built for software: Verasco
