George Pîrlea
where else to find them
no profile links on file
what they talk about
all 6 in the filters
where they keep going back
no series more than once — all 4 in the filters
on a stage with
all 10 in the filters
who talks about the same things
nobody close enough yet
| title | conference | date |
|---|---|---|
| Velvet: A Multi-Modal Verifier for Effectful Programs | Dafny 2026 | 2026-01-11 |
Velvet is a Dafny-style verifier implemented as a Lean library that verifies imperative programs with mutable state, loops, and nondeterminism by generating… | ||
| Lessons from Building an Auto-Active Verifier in Lean | Dafny 2026 | 2026-01-11 |
Veil is an auto‑active verifier implemented as a Lean library that does concrete and symbolic model checking, bounded searches, and inductive‑invariant… | ||
| Foundational Multi-Modal Program Verifiers | POPL 2026 | 2026-01-11 |
Paper presents a framework implemented in Lean implementation that provides a library of monad transformers for state, divergence, exceptions and… | ||
| Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separatio... | CPP 2024 | 2024-01-15 |
Provides a library of definitions, lemmas and proof rules that let one switch between array and tree views (mutually derivable) to localize updates, formalizes… | ||
| Certifying the Synthesis of Heap-Manipulating Programs | SPLASH 2022 | 2022-12-05 |
Method translates SuSLik synthesis traces into machine-checkable Coq proofs and produces three certifiers for HTT, Iris and VST, evaluated on 15 benchmarks… | ||
| Practical Smart Contract Sharding with Ownership and Commutativity Analysis | SPLASH 2022 | 2022-12-05 |
Static analysis tool CoSplit infers per-transition ownership and commutativity summaries for Cilla smart contracts and compiles them into sharding signatures… | ||
| nothing matches | ||