Andrea Lattuada
where else to find them
what they talk about
all 6 in the filters
where they keep going back
all 8 in the filters
on a stage with
all 38 in the filters
who talks about the same things
- Derek Dreyer35 talks
- Ralf Jung18 talks
- Ranjit Jhala19 talks
- Robbert Krebbers26 talks
- Jonathan Aldrich17 talks
- Jonáš Fiala4 talks
| title | conference | date |
|---|---|---|
| Tunable Automation in Automated Program Verification | Dafny 2026 | 2026-01-11 |
A Rust-based verifier (Verus) adds a broadcast lemmas mechanism to let libraries export grouped, universally quantified facts and users import them at module… | ||
| Destabilizing Iris | PLDI 2025 | 2025-06-16 |
Adds Daenerys to Iris: a reworked resource layer that introduces unstable resources and an explicit frame modality, plus an unstable points-to and a… | ||
| Anvil: Verifying Liveness of Cluster Management Controllers | 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI '24) | 2024-07-10 |
Anvil presents eventually stable reconciliation as a concise temporal liveness spec and provides a Rust framework that verifies controllers against it using… | ||
| Domesticating Automation | Dafny 2024 | 2024-01-14 |
Proposes a module-granular view of the quantifier instantiation graph and a crude metric that ranks modules by how many downstream instantiations they enable… | ||
| Verus: Verifying Rust Programs using Linear Ghost Types | OOPSLA 2023 | 2023-10-23 |
Verus is an SMT-based verifier that embeds proofs in Rust and uses linear ghost permissions to represent ownership-aligned memory permissions; the tool demands… | ||
| Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent System | OSDI 2023 | 2023-07-10 |
IronSync is an automated verification framework that uses an ownership type system and a Localized Transition System to split global proofs into small… | ||
| Linear types for large-scale systems verification | OOPSLA 2022 | 2022-12-05 |
Integrates linear Dafny with Dafny's SMT backend to push memory reasoning into the type system while keeping SMT for heap invariants; implements… | ||
| SnailTrail: Generalizing Critical Paths for Online Analysis of Distributed Dataflows | NSDI '18 | 2018-04-09 |
System generalizes critical path analysis to streaming jobs and reports a per-activity critical participation score computed on time-based windows from a… | ||
| A hammer you can only hold by the handle | RustFest Zürich 2017 | 2017-09-30 |
Claim: Rust’s type system enforces concrete API invariants at compile time. It uses affine types and non-Clone structs as tokens so operations consume values… | ||
| TYPECLASSES — A TYPE SYSTEM CONSTRUCT | Scalar Conference 2017 | 2017-04-07 |
Typeclasses provide ad hoc polymorphism in Scala but are implemented via implicits, which creates surprises: orphan instances roam globally, implicit search… | ||
| nothing matches | ||