Arie Gurfinkel
where else to find them
what they talk about
where they keep going back
- VMCAI2 editions2022–2025
all 5 in the filters
on a stage with
all 13 in the filters
who talks about the same things
- Grigory Fedyukovich4 talks
- Ranjit Jhala19 talks
- Joshua Gancher6 talks
- Sharon Shoham13 talks
- Lennard Gäher7 talks
- Klaus von Gleissenthall5 talks
| title | conference | date |
|---|---|---|
| A Flow-Sensitive Refinement Type System for Verifying eBPF Programs | OOPSLA 2025 | 2025-10-16 |
Type-based verifier infers proof certificates in userspace and pushes only a small checker into the kernel, reducing the trusted codebase. Implementation… | ||
| Automatic Inference of Relational Object Invariants | VMCAI 2025 | 2025-01-20 |
Claims an Abstract Interpretation method that infers relational object invariants by splitting memory into banks and keeping a most-recently-used cache entry… | ||
| Compositional Verification of Smart Contracts Through Communication Abstraction | SPLASH 2022 | 2022-12-05 |
Claims that local bundles reduce contracts with 2^160 addresses to a sequential C model with a handful of representative users computed via static analysis… | ||
| Verifying Solidity Smart Contracts Via Communication Abstraction in SmartACE | VMCAI 2022 | 2022-01-16 |
SmartACE is an automated pipeline that translates Solidity + Scribble specs to an LLVM harness and applies parametrized verification via local bundle… | ||
| Solving Constrained Horn Clauses Modulo Algebraic Data Types and Recursive Funct | POPL 2022 | 2022-01-16 |
Presents an IC3/PDR-inspired solver called Racer that combines relationification, controlled unfolding of recursive definitions, and uninterpreted-function… | ||
| Compositional Verification of Smart Contracts Through Communication Abstraction | SAS 2021 | 2021-10-17 |
Claims a local bundle abstraction that reduces Solidity contracts with 2^160 addresses to a few representative users (example: 2^160 → 4) and turns… | ||
| nothing matches | ||