| 2026 | CAV | Lagrangian-Based Duality for Quantified SMT Algorithms. | Ivana Bocevska, Takeshi Tsukada, Hiroshi Unno, Oded Padon, Sharon Shoham |
| 2026 | ESOP | A Category-Theoretic Framework for Dependent Effect Systems. | Satoshi Kura, Marco Gaboardi, Taro Sekiyama, Hiroshi Unno |
| 2026 | SAT | Exact Symbolic Reasoning for Nonlinear Stochastic SMT via Cylindrical Algebraic Decomposition. | Jung-Cheng Lin, Chia-Hsuan Su, Jie-Hong R. Jiang, Hiroshi Unno |
| 2025 | AAAI | Solving Higher-Order Quantified Boolean Satisfiability via Higher-Order Model Checking. | Hiroshi Unno, Takeshi Tsukada, Jie-Hong Roland Jiang |
| 2021 | CAV | Decision Tree Learning in CEGIS-Based Termination Analysis. | Satoshi Kura, Hiroshi Unno, Ichiro Hasuo |
| 2021 | CAV | Constraint-Based Relational Verification. | Hiroshi Unno, Tachio Terauchi, Eric Koskinen |
| 2021 | SAS | Toward Neural-Network-Guided Program Synthesis and Verification. | Naoki Kobayashi, Taro Sekiyama, Issei Sato, Hiroshi Unno |
| 2020 | AAAI | Probabilistic Inference for Predicate Constraint Satisfaction. | Yuki Satake, Hiroshi Unno, Hinata Yanagi |
| 2019 | SAS | Temporal Verification of Programs via First-Order Fixpoint Logic. | Naoki Kobayashi, Takeshi Nishikawa, Atsushi Igarashi, Hiroshi Unno |
| 2018 | CAV | Propositional Dynamic Logic for Higher-Order Functional Programs. | Yuki Satake, Hiroshi Unno |
| 2018 | LICS | A Fixpoint Logic and Dependent Effects for Temporal Property Verification. | Yoji Nanjo, Hiroshi Unno, Eric Koskinen, Tachio Terauchi |
| 2017 | CAV | Automating Induction for Solving Horn Clauses. | Hiroshi Unno, Sho Torii, Hiroki Sakamoto |
| 2016 | POPL | Temporal verification of higher-order functional programs. | Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, Hiroshi Unno |
| 2015 | APLAS | Automata-Based Abstraction for Automated Verification of Higher-Order Tree-Processing Programs. | Yuma Matsumoto, Naoki Kobayashi, Hiroshi Unno |
| 2015 | CAV | Predicate Abstraction and CEGAR for Disproving Termination of Higher-Order Functional Programs. | Takuya Kuwahara, Ryosuke Sato, Hiroshi Unno, Naoki Kobayashi |
| 2015 | ESOP | Relaxed Stratification: A New Approach to Practical Complete Predicate Refinement. | Tachio Terauchi, Hiroshi Unno |
| 2015 | IWDW | Nondestructive Readout of Copyright Information Embedded in Objects Fabricated with 3-D Printers. | Piyarat Silapasuphakornwong, Masahiro Suzuki, Hiroshi Unno, Hideyuki Torii, Kazutake Uehira, Youichi Takashima |
| 2015 | SAS | Refinement Type Inference via Horn Constraint Optimization. | Kodai Hashimoto, Hiroshi Unno |
| 2015 | TACAS | Inferring Simple Solutions to Recursion-Free Horn Clauses via Sampling. | Hiroshi Unno, Tachio Terauchi |
| 2014 | ESOP | Automatic Termination Verification for Higher-Order Functional Programs. | Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno, Naoki Kobayashi |
| 2013 | PEPM | Towards a scalable software model checker for higher-order programs. | Ryosuke Sato, Hiroshi Unno, Naoki Kobayashi |
| 2013 | POPL | Automating relatively complete verification of higher-order functional programs. | Hiroshi Unno, Tachio Terauchi, Naoki Kobayashi |
| 2011 | PLDI | Predicate abstraction and CEGAR for higher-order model checking. | Naoki Kobayashi, Ryosuke Sato, Hiroshi Unno |
| 2010 | APLAS | Verification of Tree-Processing Programs via Higher-Order Model Checking. | Hiroshi Unno, Naoshi Tabuchi, Naoki Kobayashi |
| 2010 | POPL | Higher-order multi-parameter tree transducers and recursion schemes for program verification. | Naoki Kobayashi, Naoshi Tabuchi, Hiroshi Unno |
| 2009 | PPDP | Dependent type inference with interpolants. | Hiroshi Unno, Naoki Kobayashi |
| 2008 | FLOPS | On-Demand Refinement of Dependent Types. | Hiroshi Unno, Naoki Kobayashi |
| 2007 | MVA | Extraction of Corresponding Points from Stereo Images by Using Intersections of Segments. | Hiroshi Unno, Keikichi Hayashibe, Hitoshi Saji |
| 2006 | PLDI | Combining type-based analysis and model checking for finding counterexamples against non-interference. | Hiroshi Unno, Naoki Kobayashi, Akinori Yonezawa |
| 2002 | CW | A Real-Time Configurable Shader Based on Lookup Tables. | Eisaku Ohbuchi, Hiroshi Unno |
| 2002 | CW | A Practical Image Retouching Method. | Vladimir V. Savchenko, Nikita Kojekine, Hiroshi Unno |
| 2002 | CW | Possible Techniques for Three Dimensional Hatching. | Vladimir V. Savchenko, Hiroshi Unno, Nikita Kojekine |