Jean-Baptiste Tristan
where else to find them
no profile links on file
what they talk about
all 4 in the filters
where they keep going back
- Dafny2 editions2024–2025
- PLDI Workshop Honoring Andreas Podelski2 editions2023–2025
on a stage with
all 18 in the filters
who talks about the same things
- Joseph Tassarotti20 talks
- Gilles Barthe17 talks
- Markus de Medeiros3 talks
- Justin Hsu13 talks
- Adam Chlipala23 talks
- David Darais5 talks
| title | conference | date |
|---|---|---|
| Verified Foundations for Differential Privacy | PLDI 2025 | 2025-06-16 |
SampCert is a mechanized foundation for differential privacy written in Lean that proves correctness of sampling and DP composition and ships verified samplers… | ||
| Verifying the Fisher-Yates Shuffle Algorithm in Dafny | Dafny 2025 | 2025-01-19 |
Verified Fisher‑Yates implementation in Dafny defines a functional model on bitstreams, proves it yields each permutation with probability 1/n! for… | ||
| Performant, Readable and Interoperable Rust from Dafny | Dafny 2025 | 2025-01-19 |
A Dafny-to-Rust compiler that emits largely readable Rust code, uses a postprocessing pass to reuse local names and factor absolute paths into imports, and… | ||
| Randomised Testing of the Dafny Compiler | Dafny 2024 | 2024-01-14 |
Built two generators, fuzz-d (differential testing) and DafnyFuzz (metamorphic testing), plus comparison with XDsmith, and apply reconditioning and… | ||
| VMC: a Dafny Library for Verified Monte Carlo Algorithms | Dafny 2024 | 2024-01-14 |
Open-source Dafny library that provides verified Monte Carlo samplers: each sampler has a bitstream-to-value functional model, a machine-checked proof that the… | ||
| Generation of Verified Assembly Code Using Dafny and Reinforcement Learning | Dafny 2024 | 2024-01-14 |
Reinforcement learning generates assembly programs while a Dafny model of machine state automatically verifies input-output properties, turning testing into… | ||
| Verified Density Compilation for a Probabilistic Programming Language | PLDI 2023 | 2023-06-17 |
Provides a mechanized semantics for a Stan subset and verifies three density-compilation passes in Coq, producing ProbCompCert that connects to CompCert down… | ||
| nothing matches | ||