Benjamin Bonneau
where else to find them
what they talk about
where they keep going back
no series more than once — all 2 in the filters
on a stage with
all 8 in the filters
who talks about the same things
- Gaurav Parthasarathy3 talks
- David Monniaux7 talks
- Sylvain Boulmé4 talks
- Thibault Dardinier9 talks
- Eric Mugnier4 talks
- Benjamin Gregoire6 talks
| title | conference | date |
|---|---|---|
| Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into(…) | PLDI 2024 | 2024-06-24 |
Adds a per-run Isabelle certificate generator to an existing Viper→Boogie translation, proving that whenever the generated Boogie program has no failing… | ||
| Formally Verifying Optimizations with Block Simulations | OOPSLA 2023 | 2023-10-23 |
Framework implements block-level forward simulations inside CompCert and proves validators in the Coq proof assistant that check concrete morphisms between… | ||
| nothing matches | ||