David Pichardie
where else to find them
what they talk about
where they keep going back
all 4 in the filters
on a stage with
all 9 in the filters
who talks about the same things
- Sandrine Blazy6 talks
- Aurèle Barrière7 talks
- Olivier Flückiger7 talks
- Adam Chlipala23 talks
- Manas Thakur9 talks
- Jan Vitek26 talks
| title | conference | date |
|---|---|---|
| Current State of the Industrial-Strength Infer Static Analysis Platform | VMCAI 2026 | 2026-01-12 |
Infer is an industrial static analyzer with 15+ years of production use, running daily in CI against thousands of developers and 10+ million LOC with hundreds… | ||
| Contextual Equality Saturation | SAS 2025 | 2025-10-13 |
Extends equality saturation so rewriting can occur under local branch assumptions, replacing costly swap laws with contextual rewriting rules that match a… | ||
| Enhancing Infer Compositional Analysis with Summary Specialization | TPSA 2025 | 2025-01-19 |
Infer adds summary specialization to its compositional, on‑demand bottom‑up analyzer: compute per‑function summaries under lightweight assumptions… | ||
| Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCe... | POPL 2023 | 2023-01-15 |
Prototype JIT is implemented and mechanically verified in Coq, reusing the CompCert backend and its correctness proofs to generate x86 code, and modeling… | ||
| A Flow-Insensitive-Complete Program Representation | VMCAI 2022 | 2022-01-16 |
Claims a program transformation that makes a flow‑insensitive analysis as precise as a flow‑sensitive one for assertion failures under pure collecting… | ||
| Verified Functional Programming of an Abstract Interpreter | SAS 2021 | 2021-10-17 |
Claims a fully implemented abstract interpreter in the F verified programming environment that proves soundness while keeping proofs tiny: about 40 lines of… | ||
| Formally Verified Speculation and Deoptimization in a JIT Compiler | POPL 2021 | 2021-01-17 |
A formal model defines a JIT’s middle end, an RTL-like IR and two concrete speculative ops: the anchor instruction which marks safe deoptimization points and… | ||
| nothing matches | ||