Jorge A. Navas
where else to find them
no profile links on file
what they talk about
where they keep going back
- VMCAI2 editions2022–2025
all 4 in the filters
on a stage with
all 15 in the filters
who talks about the same things
nobody close enough yet
| 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… | ||
| 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… | ||
| Disjunctive Interval Analysis | SAS 2021 | 2021-10-17 |
Proposes range decision diagrams (RDDs) as a compact Boxes implementation that avoids constraint substitution and no dependence on a theory solver, and that… | ||
| nothing matches | ||