Hiroshi Unno

56 papers A* 7A 3B 5C 2Misc 1Journal 31Unranked 7
YearRankTypeTitle / Venue / Authors
2026 — conf
A Category-Theoretic Framework for Dependent Effect Systems.
ESOP (1)
Satoshi Kura, Marco Gaboardi, Taro Sekiyama, Hiroshi Unno
2026 J jnl
A Category-Theoretic Framework for Dependent Effect Systems.
CoRR
Satoshi Kura, Marco Gaboardi, Taro Sekiyama, Hiroshi Unno
2025 J jnl
A Denotational Product Construction for Temporal Verification of Effectful Higher-Order Programs.
CoRR
Kazuki Watanabe, Mayuko Kori, Taro Sekiyama, Satoshi Kura, Hiroshi Unno
2025 J jnl
A Hierarchy of Supermartingales for ω-Regular Verification.
CoRR
Satoshi Kura, Hiroshi Unno
2025 J jnl
A Primal-Dual Perspective on Program Verification Algorithms (Extended Version).
CoRR
Takeshi Tsukada, Hiroshi Unno, Oded Padon, Sharon Shoham
2025 J jnl
A Primal-Dual Perspective on Program Verification Algorithms.
Proc. ACM Program. Lang.
Takeshi Tsukada, Hiroshi Unno, Oded Padon, Sharon Shoham
2025 J jnl
Algebraic Temporal Effects: Temporal Verification of Recursively Typed Higher-Order Programs.
Proc. ACM Program. Lang.
Taro Sekiyama, Hiroshi Unno
2025 J jnl
On Higher-Order Model Checking of Effectful Answer-Type-Polymorphic Programs.
Proc. ACM Program. Lang.
Taro Sekiyama, Ugo Dal Lago, Hiroshi Unno
2025 J jnl
Ranking and Invariants for Lower-Bound Inference in Quantitative Verification of Probabilistic Programs.
CoRR
Satoshi Kura, Hiroshi Unno, Takeshi Tsukada
2025 A* conf
Solving Higher-Order Quantified Boolean Satisfiability via Higher-Order Model Checking.
AAAI
Hiroshi Unno, Takeshi Tsukada, Jie-Hong Roland Jiang
2025 J jnl
Thrust: A Prophecy-Based Refinement Type System for Rust.
Proc. ACM Program. Lang.
Hiromi Ogawa, Taro Sekiyama, Hiroshi Unno
2025 J jnl
Towards neural-network-guided program synthesis and verification.
Formal Methods Syst. Des.
Naoki Kobayashi, Taro Sekiyama, Issei Sato, Hiroshi Unno
2024 J jnl
Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers.
Proc. ACM Program. Lang.
Fuga Kawamata, Hiroshi Unno, Taro Sekiyama, Tachio Terauchi
2024 J jnl
Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System.
CoRR
Satoshi Kura, Hiroshi Unno
2024 J jnl
Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System.
Proc. ACM Program. Lang.
Satoshi Kura, Hiroshi Unno
2024 J jnl
Higher-Order Model Checking of Effect-Handling Programs with Answer-Type Modification.
Proc. ACM Program. Lang.
Taro Sekiyama, Hiroshi Unno
2024 J jnl
Inductive Approach to Spacer.
Proc. ACM Program. Lang.
Takeshi Tsukada, Hiroshi Unno
2023 J jnl
Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers.
CoRR
Fuga Kawamata, Hiroshi Unno, Taro Sekiyama, Tachio Terauchi
2023 J jnl
Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification.
Proc. ACM Program. Lang.
Hiroshi Unno, Tachio Terauchi, Yu Gu, Eric Koskinen
2023 J jnl
Optimal CHC Solving via Termination Proofs.
Proc. ACM Program. Lang.
Yu Gu, Takeshi Tsukada, Hiroshi Unno
2023 J jnl
Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations.
Proc. ACM Program. Lang.
Taro Sekiyama, Hiroshi Unno
2022 J jnl
Software model-checking as cyclic-proof search.
Proc. ACM Program. Lang.
Takeshi Tsukada, Hiroshi Unno
2022 J jnl
Temporal Verification with Answer-Effect Modification.
CoRR
Taro Sekiyama, Hiroshi Unno
2021 — conf
Constraint-Based Relational Verification.
CAV (1)
Hiroshi Unno, Tachio Terauchi, Eric Koskinen
2021 J jnl
Constraint-based Relational Verification.
CoRR
Hiroshi Unno, Tachio Terauchi, Eric Koskinen
2021 — conf
Decision Tree Learning in CEGIS-Based Termination Analysis.
CAV (2)
Satoshi Kura, Hiroshi Unno, Ichiro Hasuo
2021 J jnl
Decision Tree Learning in CEGIS-Based Termination Analysis.
CoRR
Satoshi Kura, Hiroshi Unno, Ichiro Hasuo
2021 J jnl
Enhancing Loop-Invariant Synthesis via Reinforcement Learning.
CoRR
Takeshi Tsukada, Hiroshi Unno, Taro Sekiyama, Kohei Suenaga
2021 J jnl
Software Model-Checking as Cyclic-Proof Search.
CoRR
Takeshi Tsukada, Hiroshi Unno
2021 B conf
Toward Neural-Network-Guided Program Synthesis and Verification.
SAS
Naoki Kobayashi, Taro Sekiyama, Issei Sato, Hiroshi Unno
2021 J jnl
Toward Neural-Network-Guided Program Synthesis and Verification.
CoRR
Naoki Kobayashi, Taro Sekiyama, Issei Sato, Hiroshi Unno
2020 A* conf
Probabilistic Inference for Predicate Constraint Satisfaction.
AAAI
Yuki Satake, Hiroshi Unno, Hinata Yanagi
2020 J jnl
Program Verification via Predicate Constraint Satisfiability Modulo Theories.
CoRR
Hiroshi Unno, Yuki Satake, Tachio Terauchi, Eric Koskinen
2019 B conf
Temporal Verification of Programs via First-Order Fixpoint Logic.
SAS
Naoki Kobayashi, Takeshi Nishikawa, Atsushi Igarashi, Hiroshi Unno
2018 A* conf
A Fixpoint Logic and Dependent Effects for Temporal Property Verification.
LICS
Yoji Nanjo, Hiroshi Unno, Eric Koskinen, Tachio Terauchi
2018 — conf
Propositional Dynamic Logic for Higher-Order Functional Programs.
CAV (1)
Yuki Satake, Hiroshi Unno
2018 J jnl
Relatively complete refinement type system for verification of higher-order non-deterministic programs.
Proc. ACM Program. Lang.
Hiroshi Unno, Yuki Satake, Tachio Terauchi
2017 — conf
Automating Induction for Solving Horn Clauses.
CAV (2)
Hiroshi Unno, Sho Torii, Hiroki Sakamoto
2016 J jnl
Automating Induction for Solving Horn Clauses.
CoRR
Hiroshi Unno, Sho Torii
2016 A* conf
Temporal verification of higher-order functional programs.
POPL
Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, Hiroshi Unno
2015 B conf
Automata-Based Abstraction for Automated Verification of Higher-Order Tree-Processing Programs.
APLAS
Yuma Matsumoto, Naoki Kobayashi, Hiroshi Unno
2015 A conf
Inferring Simple Solutions to Recursion-Free Horn Clauses via Sampling.
TACAS
Hiroshi Unno, Tachio Terauchi
2015 — conf
Predicate Abstraction and CEGAR for Disproving Termination of Higher-Order Functional Programs.
CAV (2)
Takuya Kuwahara, Ryosuke Sato, Hiroshi Unno, Naoki Kobayashi
2015 B conf
Refinement Type Inference via Horn Constraint Optimization.
SAS
Kodai Hashimoto, Hiroshi Unno
2015 J jnl
Refinement Type Inference via Horn Constraint Optimization.
CoRR
Kodai Hashimoto, Hiroshi Unno
2015 A conf
Relaxed Stratification: A New Approach to Practical Complete Predicate Refinement.
ESOP
Tachio Terauchi, Hiroshi Unno
2015 J jnl
Verification of tree-processing programs via higher-order mode checking.
Math. Struct. Comput. Sci.
Hiroshi Unno, Naoshi Tabuchi, Naoki Kobayashi
2014 A conf
Automatic Termination Verification for Higher-Order Functional Programs.
ESOP
Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno, Naoki Kobayashi
2013 A* conf
Automating relatively complete verification of higher-order functional programs.
POPL
Hiroshi Unno, Tachio Terauchi, Naoki Kobayashi
2013 C conf
Towards a scalable software model checker for higher-order programs.
PEPM
Ryosuke Sato, Hiroshi Unno, Naoki Kobayashi
2011 A* conf
Predicate abstraction and CEGAR for higher-order model checking.
PLDI
Naoki Kobayashi, Ryosuke Sato, Hiroshi Unno
2010 A* conf
Higher-order multi-parameter tree transducers and recursion schemes for program verification.
POPL
Naoki Kobayashi, Naoshi Tabuchi, Hiroshi Unno
2010 B conf
Verification of Tree-Processing Programs via Higher-Order Model Checking.
APLAS
Hiroshi Unno, Naoshi Tabuchi, Naoki Kobayashi
2009 C conf
Dependent type inference with interpolants.
PPDP
Hiroshi Unno, Naoki Kobayashi
2008 Misc conf
On-Demand Refinement of Dependent Types.
FLOPS
Hiroshi Unno, Naoki Kobayashi
2006 — conf
Combining type-based analysis and model checking for finding counterexamples against non-interference.
PLAS
Hiroshi Unno, Naoki Kobayashi, Akinori Yonezawa