Andrew W. Appel
where else to find them
no profile links on file
what they talk about
where they keep going back
on a stage with
- Ariel E. Kellisononce
- Jianxing Qinonce
- Joomy Korkutonce
all 7 in the filters
who talks about the same things
- Kathrin Stark8 talks
- Qinxiang Cao8 talks
- Théo Winterhalter14 talks
- Jérémie Koenig4 talks
- Adam Chlipala23 talks
- Peter Sewell14 talks
| title | conference | date |
|---|---|---|
| A Verified Foreign Function Interface Between Coq and C | POPL 2025 | 2025-01-19 |
VeriFFI provides a verified foreign-function interface that translates Coq dependent types and Coq functional models into VST specs so C functions, once proved… | ||
| VCFloat2: Floating-point error analysis in Coq | CPP 2024 | 2024-01-15 |
VCFloat2 is a Coq tool that automatically and soundly computes floating‑point round‑off error bounds with computational reflection, handling nonstandard… | ||
| VST-A: A Foundationally Sound Annotation Verifier | POPL 2024 | 2024-01-14 |
VST-A is an annotation verifier that parses C into control‑flow graphs, splits functions into paths (four paths for the linked‑list reverse example) and… | ||
| Coq's vibrant ecosystem for verification engineering | CPP 2022 | 2022-01-17 |
Coq now supports end-to-end, layered verification: a Verified Software Toolchain connects C proofs to the CompCert semantics and backends like CompCert and… | ||
| nothing matches | ||