Eric Koskinen
where else to find them
bluesky:erickoskinen.bsky.social
what they talk about
all 4 in the filters
where they keep going back
all 6 in the filters
on a stage with
all 23 in the filters
who talks about the same things
- Timos Antonopoulos5 talks
- Ton Chanh Le8 talks
- Hiroshi Unno18 talks
- Sharon Shoham13 talks
- Takeshi Tsukada16 talks
- Michael Sammler16 talks
| title | conference | date |
|---|---|---|
| Relational Cell Morphing: Automated Verification of Relational Properties of Array(…) | ARRAY 2026 | 2026-06-16 |
The system reduces relational verification of array programs to constrained Horn clause solving over scalars by tracking a few distinguished cells across two… | ||
| Abstract Interpretation of Temporal Safety Effects of Higher Order Programs | OOPSLA 2025 | 2025-10-16 |
Introduces an abstract effect domain that summarizes context‑sensitive dependent effects as symbolic automata with accumulators, gives an abstract transformer… | ||
| An Abstract Domain for Heap Commutativity | VMCAI 2025 | 2025-01-20 |
Defines an abstract domain that lifts sets of concrete heaps into pure mathematical values (e.g., lists) via a projection pi, uses a purview to mark wellformed… | ||
| Scenario-based Proofs for Concurrent Objects | OOPSLA 2024 | 2024-10-20 |
Defines a small set of representative interleavings — the commutativity quotient — and an expression language (regular/context-free) that encodes them so… | ||
| Verifying, Inferring and Exploiting Code Commutativity | VMCAI 2023 | 2023-01-15 |
[VMCAI'23] Verifying, Inferring and Exploiting Code Commutativity
Eric Koskinen
Algebraic commutativity has long been used as an effective abstraction… | ||
| Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification | POPL 2023 | 2023-01-15 |
Reduces μCLP validity to a predicate-constraint problem and leverages an existing solver to give a sound and relatively-complete decision method, then improves… | ||
| An Algebra of Alignment for Relational Verification | POPL 2023 | 2023-01-15 |
Extends Kleene Algebra with Tests into BiKAT and shows it exactly encodes lockstep and asynchronous product alignments so relational specs reduce to algebraic… | ||
| Veracity: Declarative Multicore Programming with Commutativity | OOPSLA 2022 | 2022-12-05 |
A new language, Veracity (implemented in Multicore OCaml), lets programmers mark commute blocks with logical predicates and the compiler either forks them or… | ||
| Proving LTL Properties of Bitvector Programs and Decompiled Binaries | APLAS 2021 | 2021-10-17 |
Introduces a source transformation that replaces bitvector operators with extra linear-case splits and uses integer interpolation to let SMT-backed tools… | ||
| DynamiTe: Dynamic Termination and Non-termination Proofs | OOPSLA 2020 | 2020-11-15 |
DynamiTe is a Python tool that instruments loops with vtrace instrumentation and iteration counters, learns linear ranking functions from concrete terminating… | ||
| Demystify Today's Binary Disassembling and How Modern ABI Makes it Easier | Black Hat Asia 2020 | 2020-09-29 |
Paper reads source code of eight open tools Ghidra, Angr, McSema, Dyninst, Radare2, Jakstab, Uroboros, Objdump and documents 44 strategies (15 principled, 29… | ||
| nothing matches | ||