Hiroyuki Katsura
where else to find them
what they talk about
all 4 in the filters
where they keep going back
no series more than once — all 5 in the filters
on a stage with
all 15 in the filters
who talks about the same things
- Dhruv C. Makwana3 talks
- Rini Banerjee2 talks
- Christopher Pulte4 talks
- Ryosuke Sato10 talks
- Kayvan Memarian6 talks
- Naoki Kobayashi17 talks
| title | conference | date |
|---|---|---|
| Combining Agentic AI and Lightweight Formal Methods To Find Bugs in a Production(…) | PAgE 2026 | 2026-06-15 |
Combines the executable-spec framework for Android pKVM with an OpenAI Codex-based agent that writes ambient-C ghost code and tests, running for about one… | ||
| Code-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into(…) | PLDI 2026 | 2026-06-15 |
Integrates CN separation logic into runtime checks, unit and SMT-based random generator testing, and final machine-checked proofs, all on the real-world PKVM… | ||
| Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic(…) | SAS 2025 | 2025-10-13 |
A procedure automatically abstracts CHCs over algebraic data types to integer CHCs by synthesizing catamorphisms (generalized folds) via a CEGAR-style loop… | ||
| Higher-Order Property-Directed Reachability | ICFP 2023 | 2023-09-04 |
Formalizes a higher-order extension of PDR that extends PDR to nu-HFL(Z) so transition systems can be described by higher-order recursive functions, implements… | ||
| A New Refinement Type System for Automated nu-HFLZ Validity Checkin | SPLASH 2022 | 2022-12-05 |
A refinement type system targets validity checking for a fragment of vHFLZ (no least fixpoints) and produces template-based constraints that are solved to… | ||
| nothing matches | ||