The following pages link to Frédéric Besson (Q1687718):
Displaying 7 items.
- CompCertS: a memory-aware verified C compiler using pointer as integer semantics (Q1687720) (← links)
- A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data (Q1739908) (← links)
- \textsc{CompCertS}: a memory-aware verified C compiler using a pointer as integer semantics (Q2319992) (← links)
- A Concrete Memory Model for CompCert (Q2945624) (← links)
- Modular SMT Proofs for Fast Reflexive Checking Inside Coq (Q3100210) (← links)
- Fast Reflexive Arithmetic Tactics the Linear Case and Beyond (Q3612435) (← links)
- Itauto: An Extensible Intuitionistic SAT Solver (Q6157250) (← links)
