Hiroshi Unno
where else to find them
what they talk about
all 5 in the filters
where they keep going back
- POPL4 editions2022–2025
- PLDI Workshop Honoring Andreas Podelski3 editions2024–2026
- OOPSLA2 editions2024–2025
all 7 in the filters
on a stage with
all 15 in the filters
who talks about the same things
- Takeshi Tsukada16 talks
- Taro Sekiyama12 talks
- Tachio Terauchi4 talks
- Ugo Dal Lago14 talks
- Sharon Shoham13 talks
- Joseph Tassarotti20 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… | ||
| A Hierarchy of Supermartingales for ω-Regular Verification | PLDI 2026 | 2026-06-15 |
Defines four new certificate classes and proves a strict hierarchy: GSSMs complete for positive recurrence, DVSSMs complete for null recurrence and the most… | ||
| Supermartingales for Unique Fixed Points: A Unified Approach to Lower Bound Verification | PLDI 2026 | 2026-06-15 |
Presents a concrete criterion that turns uniqueness of least fixed points into a usable lower-bound proof: existence of a U-ranking supermartingale plus a… | ||
| On Higher-Order Model Checking of Effectful Answer-Type-Polymorphic Programs | OOPSLA 2025 | 2025-10-16 |
Claims decidability for a nontrivial fragment of effectful higher-order programs by introducing polymorphic answer-type □ and a type system that allows… | ||
| Thrust: A Prophecy-Based Refinement Type System for Rust | PLDI 2025 | 2025-06-16 |
A new Rust verifier called Thrust implements a dependent refinement type system plus an inference pipeline that emits Constrained Horn Clauses to a CHC solver… | ||
| Algebraic Temporal Effects: Temporal Verification of Recursively Typed Higher-Order(…) | POPL 2025 | 2025-01-19 |
Proposes algebraic temporal effects: an axiomatized effect algebra plus an R modality for guarded recursive types that stratifies infinite behavior, an effect… | ||
| A Primal-Dual Perspective on Program Verification Algorithms | POPL 2025 | 2025-01-19 |
Presents a unified algorithmic framework that generalizes Lagrangians to discrete domains (powersets, predicates, ranking functions) and runs an abstract… | ||
| Higher-Order Model Checking of Effect-Handling Programs with Answer-Type Modification | OOPSLA 2024 | 2024-10-20 |
Claims decidability for higher-order model checking of programs with algebraic effect handlers by statically bounding the number of simultaneously active… | ||
| Inductive Approach to Spacer | PLDI 2024 | 2024-06-24 |
Presents a Spacer-like CHC solver derived by structural induction that replaces global quantifier elimination with an iterative, lazy use of model-based… | ||
| Automating Relational Verification of Infinite-State Programs | VMCAI 2024 | 2024-01-15 |
Two automated approaches appear: a constraint-based pipeline that encodes simultaneous synthesis of a semantic scheduler and relational invariant into an… | ||
| Answer Refinement Modification: Refinement Type System for Algebraic Effects and... | POPL 2024 | 2024-01-14 |
Proposes a refinement type system that tracks how delimited-continuation effects change return types via answer refinement modification, formalizes ATM/ARM… | ||
| Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-a... | POPL 2023 | 2023-01-15 |
Extends a temporal type-and-effect system to handle delimited continuations (shift0/reset0) by tracking how continuations change the observable trace — the key… | ||
| 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… | ||
| Optimal CHC Solving via Termination Proofs | POPL 2023 | 2023-01-15 |
Presents a new optimality checker that reduces CHC maximality to program termination, encodes termination-argument synthesis (angelic strategy and… | ||
| Software Model-Checking as Cyclic-Proof Search | SPLASH 2022 | 2022-12-05 |
Claims that many software model-checking procedures are just proof-search strategies for a cyclic proof system and gives a worked mapping: symbolic execution… | ||
| Software Model-Checking as Cyclic-Proof Search | POPL 2022 | 2022-01-16 |
Claims that many software model-checking algorithms are exactly proof-search strategies for a cyclic proof system, so a single logical framework reconstructs… | ||
| Toward Neural-Network-Guided Program Synthesis and Verification | SAS 2021 | 2021-10-17 |
Proposes NeuGuS, a gray-box method that trains neural nets (four-layer; sometimes three-layer) then extracts inequalities from weights/biases to build Boolean… | ||
| nothing matches | ||