K. Rustan M. Leino
where else to find them
no profile links on file
what they talk about
where they keep going back
- Dafny2 editions2025–2026
on a stage with
- Ashay Raneonce
- Barry Bondonce
- Bryan Parnoonce
all 11 in the filters
who talks about the same things
nobody close enough yet
| title | conference | date |
|---|---|---|
| The Design of an Interactive Proof Mode for Dafny | Dafny 2026 | 2026-01-11 |
Prototype interactive proof mode for Dafny that back-translates SMT-LIB VCs (generated via Boogie and Z3) into Dafny-like goals using injected protect_ helper… | ||
| Keynote | Dafny 2025 | 2025-01-19 |
Dafny adds a boogie extractor that proves models for sets, sequences and multisets and emits Boogie axioms (it already caught a faulty multiset axiom), an… | ||
| Vale: Verifying High-Performance Cryptographic Assembly Code | 26th USENIX Security Symposium (USENIX Security '17) | 2017-08-16 |
Vale converts annotated, hand-tuned assembly into an abstract syntax tree and emits machine-checked proofs verified by an SMT-based verifier, letting the AST… | ||
| nothing matches | ||