Hiroshi UNNO

Professor at Research Institute of Electrical Communication, Tohoku University.
Visiting Professor at National Institute of Informatics.

E-Mail: hiroshi.unno AT acm.org

Professional Activities

Show more
Show less

Software

RCaml: A Refinement Type Checking and Inference Tool for OCaml [FLOPS 08] [PPDP 09] [POPL 13] [APLAS 14] [SAS 15] [POPL 18] [LICS 18] [CAV 18] [POPL 23 AEM] [POPL 24] [ICFP 24] [POPL 25 ATE] [preprint2] [preprint3]
supported by Kakenhi 25730035, 16H05856, and 20H04162
[HCVS 18 slides PDF] [HOPA 15 slides PPTX] [web demo (induction)] [code]

PCSat: A Predicate Constraint Solver based on CEGIS [AAAI 20] [CAV 21 DT] [CAV 21 TB] [POPL 23 Opt] [VMCAI 24]
supported by Kakenhi 16H05856 and 20H04162
[AiDL 22 slides PPTX] [STAIR lab ST seminar slides PDF] [code]

MuVal: A Fixpoint Logic Validity Checker based on pfwCSP Solving [CAV 21 DT] [POPL 23 Mod]
supported by Kakenhi 20H04162
[code]

MuCyc: A Fixpoint Logic Validity Checker based on Cyclic-Proof Search [CAV 17] [POPL 22] [VMCAI 24] [PLDI 24]
supported by Kakenhi 16H05856 and 20H04162
[HCVS 18 slides PDF] [web demo (induction)] [code]

MuStrat: A Fixpoint Logic Validity Checker based on Strategy Synthesis [POPL 25 Lag]
supported by Kakenhi 20H04162

EffCaml: A Transformation-based Verifier for Effectful OCaml Programs [ICFP 24] [OOPSLA 24]
supported by Kakenhi 20H04162
[code]

MoCHi: A Software Model Checker for Higher-Order Functional Programs [PLDI 11] [ML 12] [PEPM 13] [POPL 13] [ESOP 14] [TACAS 15] [ESOP 15] [CAV 15] [POPL 16]
[HOMC + CDPS 16 slides PDF] [web demo (safety)] [web demo (termination)] [web demo (non-termination)] [web demo (fair-termination)]

EHMTT Verifier: A Software Model Checker for Higher-Order Tree Processing Programs [POPL 10] [APLAS 10] [JSSST JCS 15] [MSCS 15] [APLAS 15] [preprint1]
[web demo]

Secure Information Flow Analyzer based on Type-Directed Self-Composition [PLAS 06]

Publications

The speaker is underlined

2025

A Primal-Dual Perspective on Program Verification Algorithms
Takeshi Tsukada, Hiroshi Unno, Oded Padon, and Sharon Shoham
To appear in POPL 2025.

Algebraic Temporal Effects: Temporal Verification of Recursively Typed Higher-Order Programs
Taro Sekiyama and Hiroshi Unno
To appear in POPL 2025.
[artifact]

2024

Higher-Order Model Checking of Effect-Handling Programs with Answer-Type Modification
Taro Sekiyama and Hiroshi Unno
In Proceedings of the ACM on Programming Languages, Volume 8, Issue OOPSLA2, ACM, pp.365:2662-365:2691, October, 2024.
[artifact]

Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System
Satoshi Kura and Hiroshi Unno
In Proceedings of the ACM on Programming Languages, Volume 8, Issue ICFP, ACM, pp.269:973-269:1002, August, 2024.
[arXiv] [artifact]

Inductive Approach to Spacer
Takeshi Tsukada and Hiroshi Unno
In Proceedings of the ACM on Programming Languages, Volume 8, Issue PLDI, ACM, pp.227:1979-227:2002, June, 2024.
[short version PDF] [full version PDF] [artifact]

Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers
Fuga Kawamata, Hiroshi Unno, Taro Sekiyama, and Tachio Terauchi
In Proceedings of the ACM on Programming Languages, Volume 8, Issue POPL, ACM, pp.5:115-5:147, January, 2024.
[arXiv] [artifact]

Automating Relational Verification of Infinite-State Programs
Hiroshi Unno
VMCAI 2024 Keynote
[slides PPTX] [slides PDF]

2023

Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification
Hiroshi Unno, Tachio Terauchi, Yu Gu, and Eric Koskinen
In Proceedings of the ACM on Programming Languages, Volume 7, Issue POPL, ACM, pp.72:2111-72:2140, January, 2023. Distinguished Paper Award
[short version PDF] [slides PPTX] [artifact]

Temporal Verification with Answer-Effect Modification
Taro Sekiyama and Hiroshi Unno
In Proceedings of the ACM on Programming Languages, Volume 7, Issue POPL, ACM, pp.71:2079-71:2110, January, 2023.
[arXiv] [artifact]

Optimal CHC Solving via Termination Proofs
Yu Gu, Takeshi Tsukada, and Hiroshi Unno
In Proceedings of the ACM on Programming Languages, Volume 7, Issue POPL, ACM, pp.21:604-21:631, January, 2023.
[short version PDF] [slides PPTX] [artifact]

2022

Software Model-Checking as Cyclic-Proof Search
Takeshi Tsukada and Hiroshi Unno
In Proceedings of the ACM on Programming Languages, Volume 6, Issue POPL, ACM, pp.63:1-63:29, January, 2022.
[arXiv]

2021

Toward Neural-Network-Guided Program Synthesis and Verification
Naoki Kobayashi, Taro Sekiyama, Issei Sato, and Hiroshi Unno
In Proceedings of the 28th Static Analysis Symposium (SAS 2021).
[arXiv]

Constraint-based Relational Verification
Hiroshi Unno, Tachio Terauchi, and Eric Koskinen
In Proceedings of the 33rd International Conference on Computer Aided Verification (CAV 2021), Lecture Notes in Computer Science 12759, pp.742-766 (Part I), July, 2021.
[short version PDF] [full version PDF] [25 min slides PPTX] [5 min slides PPTX] [artifact]

Decision Tree Learning in CEGIS-Based Termination Analysis
Satoshi Kura, Hiroshi Unno, and Ichiro Hasuo
In Proceedings of the 33rd International Conference on Computer Aided Verification (CAV 2021), Lecture Notes in Computer Science 12760, pp.75-98 (Part II), July, 2021.
[arXiv] [artifact]

2020

Probabilistic Inference for Predicate Constraint Satisfaction
Yuki Satake, Hiroshi Unno, and Hinata Yanagi
In Proceedings of the AAAI Conference on Artificial Intelligence (AAAI 2020), 34(02), pp.1644-1651, February, 2020. Oral presentation (acceptance rate 4.5%)
[short version PDF] [slides PPTX] [slides PDF]

Failure of Cut-Elimination in Cyclic Proofs of Separation Logic
Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, and Hiroshi Unno
In Journal of Computer Software, Vol. 37, No. 1, pp.1_39-1_52, 2020.

2019

Temporal Verification of Programs via First-Order Fixpoint Logic
Naoki Kobayashi, Takeshi Nishikawa, Atsushi Igarashi, and Hiroshi Unno
In Proceedings of the 26th International Static Analysis Symposium (SAS 2019), Lecture Notes in Computer Science 11822, pp.413-436, Porto, Portugal, October, 2019.

2018

Propositional Dynamic Logic for Higher-Order Functional Programs
Yuki Satake and Hiroshi Unno
In Proceedings of the 30th International Conference on Computer Aided Verification (CAV 2018), Lecture Notes in Computer Science 10981, pp.1-19 (Part I), Oxford, UK, July, 2018.
[short version PDF] [slides PDF]

A Fixpoint Logic and Dependent Effects for Temporal Property Verification
Yoji Nanjo, Hiroshi Unno, Eric Koskinen, and Tachio Terauchi
In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018), ACM, pp.759-768, Oxford, UK, July, 2018.
[short version PDF] [full version PDF] [slides PDF]

Relatively Complete Refinement Type System for Verification of Higher-Order Non-deterministic Programs
Hiroshi Unno, Yuki Satake, and Tachio Terauchi
In Proceedings of the ACM on Programming Languages, Volume 2, Issue POPL, ACM, pp.12:1-12:29, December, 2017.
[short version PDF] [slides PPTX] [slides PDF]

2017

Automating Induction for Solving Horn Clauses
Hiroshi Unno, Sho Torii, and Hiroki Sakamoto
In Proceedings of the 29th International Conference on Computer Aided Verification (CAV 2017), Lecture Notes in Computer Science 10427, pp.571-591 (Part II), Heidelberg, Germany, July, 2017.
[short version PDF] [slides PPTX] [slides PDF] [web demo]

2016

Temporal Verification of Higher-order Functional Programs
Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, and Hiroshi Unno
In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016), pp.57-68, St. Petersburg, Florida, USA, January, 2016.
[short version PDF] [web demo]

2015

Automata-Based Abstraction for Automated Verification of Higher-Order Tree-Processing Programs
Yuma Matsumoto, Naoki Kobayashi, and Hiroshi Unno
In Proceedings of the 13th Asian Symposium on Programming Languages and Systems (APLAS 2015), Lecture Notes in Computer Science 9458, pp.295-312, Pohang, South Korea, November/December, 2015.
[short version PDF]

Refinement Type Inference via Horn Constraint Optimization
Kodai Hashimoto and Hiroshi Unno
In Proceedings of the 22nd International Static Analysis Symposium (SAS 2015), Lecture Notes in Computer Science 9291, pp.199-216, Saint-Malo, France, September, 2015.
[short version PDF] [full version PDF] [slides PPTX] [slides PDF]

Predicate Abstraction and CEGAR for Disproving Termination of Higher-order Functional Programs
Takuya Kuwahara, Ryosuke Sato, Hiroshi Unno, and Naoki Kobayashi
In Proceedings of the 27th International Conference on Computer Aided Verication (CAV 2015), Lecture Notes in Computer Science 9207, pp.287-303, San Francisco, USA, July, 2015.
[short version PDF] [web demo]

Verification of Tree-Processing Programs via Higher-Order Model Checking
Hiroshi Unno, Naoshi Tabuchi, and Naoki Kobayashi
In Mathematical Structures in Computer Science, Volume 25, Special Issue 04, pp.841-866, May 2015. (accepted Jan 2012)

Inferring Simple Solutions to Recursion-free Horn Clauses via Sampling
Hiroshi Unno and Tachio Terauchi
In Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015), Lecture Notes in Computer Science 9035, pp.149-163, London, UK, April, 2015.
[short version PDF] [full version PDF] [slides PPTX] [experiment data]

Relaxed Stratification: A New Approach to Practical Complete Predicate Refinement
Tachio Terauchi and Hiroshi Unno
In Proceedings of the 24th European Symposium on Programming (ESOP 2015), Lecture Notes in Computer Science 9032, pp.610-633, London, UK, April, 2015.
[short version PDF] [full version PDF]

Counterexample Finding and Abstraction Refinement for Automated Verification of Higher-Order Transducers
Yuma Matsumoto, Naoki Kobayashi, and Hiroshi Unno
In Journal of Computer Software, Vol. 32, No. 1, pp.1_161-1_178, 2015. (in Japanese) (PPL 2014 best paper)

2014

Refinement Type Inference via Multi-Objective Optimization Subject to Horn Clauses (Poster Presentation)
Kodai Hashimoto and Hiroshi Unno
Presented at the 12th Asian Symposium on Programming Languages and Systems (APLAS 2014), Singapore, November, 2014.
[poster PDF]

Automatic Termination Verification for Higher-Order Functional Programs
Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno, and Naoki Kobayashi
In Proceedings of the 23rd European Symposium on Programming (ESOP 2014), Lecture Notes in Computer Science 8410, pp.392-411, Grenoble, France, April, 2014.
[short version PDF] [full version PDF] [web demo]

2013

Automating Relatively Complete Verification of Higher-Order Functional Programs
Hiroshi Unno, Tachio Terauchi, Naoki Kobayashi
In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2013), pp.75-86, Rome, Italy, January, 2013.
[short version PDF] [full version PDF] [slides PPTX] [web demo]

Towards a Scalable Software Model Checker for Higher-Order Programs
Ryosuke Sato, Hiroshi Unno, and Naoki Kobayashi
In Proceedings of the ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation (PEPM 2013), pp.53-62, Rome, Italy, January, 2013.
[short version PDF] [web demo]

2012

MoCHi: Software Model Checker for a Higher-Order Functional Language (Demo Presentation)
Ryosuke Sato, Hiroshi Unno, and Naoki Kobayashi
Presented at the 2012 ACM SIGPLAN Workshop on ML (ML 2012), Copenhagen, Denmark, September, 2012.
[PDF] [web demo]

2011

Predicate Abstraction and CEGAR for Higher-Order Model Checking
Naoki Kobayashi, Ryosuke Sato, and Hiroshi Unno (alphabetically ordered)
In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2011), pp.222-233, San Jose, USA, June, 2011.
[short version PDF] [full version PDF] [web demo]

2010

Verification of Tree-Processing Programs via Higher-Order Model Checking
Hiroshi Unno, Naoshi Tabuchi, and Naoki Kobayashi
In Proceedings of the 8th Asian Symposium on Programming Languages and Systems (APLAS 2010), Springer, Lecture Notes in Computer Science 6461, pp.312-327, Shanghai, China, November/December, 2010.
[short version PDF] [full version PDF] [web demo]

Resource Usage Verification for a Programming Language with Pointers
Shinpei Ueno, Naoki Kobayashi, and Hiroshi Unno
In IPSJ Transactions on Programming, Vol.3, No.4, pp.27-42, September, 2010. (in Japanese)

Higher-Order Multi-Parameter Tree Transducers and Recursion Schemes for Program Verification
Naoki Kobayashi, Naoshi Tabuchi, and Hiroshi Unno (alphabetically ordered)
In Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2010), pp.495-507, Madrid, Spain, January, 2010.
[short version PDF] [full version PDF]

2009

Dependent Type Inference with Interpolants
Hiroshi Unno and Naoki Kobayashi
In Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP 2009), pp.277-288, Coimbra, Portugal, September, 2009.
[short version PDF] [full version PDF]

2008

On-Demand Refinement of Dependent Types
Hiroshi Unno and Naoki Kobayashi
In Proceedings of the 9th International Symposium on Functional and Logic Programming (FLOPS 2008), Springer, Lecture Notes in Computer Science 4989, pp.81-96, Ise, Japan, April, 2008.
[short version PDF] [full version PDF]

2006

Combining Type-Based Analysis and Model Checking for Finding Counterexamples against Non-Interference
Hiroshi Unno, Naoki Kobayashi, and Akinori Yonezawa
In Proceedings of the ACM SIGPLAN Workshop on Programming Languages and Analysis for Security (PLAS 2006), pp.17-26, Ottawa, Canada, June, 2006.
[short version PDF] [full version PDF]

Preprints

3. Games Programs Play: Analyzing Multiplayer Programs
with Eric Koskinen and Moshe Vardi

2. Automating Total Correctness Verification of Higher-Order Functional Programs with Algebraic Data Types
with Kodai Hashimoto and Sho Torii

1. Inference of Tree Data Structure Invariant based on Language Identification from Samples
with Naoshi Tabuchi and Naoki Kobayashi
[short version PDF] [web demo]