Samuel Gruetter
where else to find them
what they talk about
all 5 in the filters
where they keep going back
no series more than once — all 4 in the filters
on a stage with
all 11 in the filters
who talks about the same things
- Andres Erbsen5 talks
- Adam Chlipala23 talks
- Gaurav Parthasarathy3 talks
- Dustin Jamner3 talks
- Adithya Murali6 talks
- Lennard Gäher7 talks
| title | conference | date |
|---|---|---|
| Live Verification in an Interactive Proof Assistant | PLDI 2024 | 2024-06-24 |
Prototype implements live verification after each line inside Coq, parsing polyglot C/Coq files and updating a concise symbolic state view while editing; it… | ||
| Foundational Integration Verification of a Cryptographic Server | PLDI 2024 | 2024-06-24 |
A verified bare-metal garage-door server implements authenticated open/close commands and prevents replays by rotating seeds, and a single machine-checked… | ||
| Flexible Instruction-Set Semantics via Abstract Monads | ICFP 2023 | 2023-09-04 |
Claims a single Haskell-based core semantics, parameterized by a Risk5Machine type class over monads, supports testing, interactive proof, model checking and… | ||
| Omnisemantics: Smooth Handling of Nondeterminism (Invited talk) | CoqPL 2023 | 2023-01-21 |
Defines operational judgments that map a start state to a set of outcomes so one derivation captures every nondeterministic run, formalized in Coq and used… | ||
| Formal Methods for Hardware Software Integration on RISC V Embedded Systems | RISC-V Summit 2019 | 2019-12-09 |
A complete digital stack — pipeline RISC‑V CPU plus software image — runs on an FPGA implementation connected to an Ethernet controller and a power switch to… | ||
| nothing matches | ||