Hiroshi UNNO

Associate Professor at Programming Logic Group , Department of Computer Science , Graduate School of Systems and Information Engineering , University of Tsukuba.

E-Mail: uhiro AT cs.tsukuba.ac.jp

Software

RCaml: Refinement Type Checking and Inference System based on Horn Constraint Solving [FLOPS 08] [PPDP 09] [POPL 13] [APLAS 14] [TACAS 15] [SAS 15] [CAV 17] [POPL 18] [preprint2] [preprint3] [preprint4]
supported by Kakenhi 25730035 and 16H05856
[slides PPTX] [web demo (induction)]

MoCHi: Software Model Checker for Higher-Order Functional Programs [PLDI 11] [ML 12] [PEPM 13] [ESOP 14] [ESOP 15] [CAV 15] [POPL 16]
supported by Kakenhi 23220001 and 15H05706
[slides PDF] [web demo (safety)] [web demo (termination)] [web demo (non-termination)] [web demo (fair-termination)]

EHMTT Verifier: Software Model Checker for Higher-Order Tree Processing Programs [POPL 10] [APLAS 10] [JSSST JCS 15] [MSCS 15] [preprint1] [APLAS 15]
supported by Kakenhi 23220001 and 15H05706
[web demo]

Secure Information Flow Analyzer based on Type-Directed Self-Composition [PLAS 06]
supported by Kakenhi 17300003

Publications

The speaker is underlined

2018

Relatively Complete Refinement Type System for Verification of Higher-Order Non-deterministic Programs
Hiroshi Unno, Yuki Satake, and Tachio Terauchi
To appear in POPL 2018.

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.
[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.

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.

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
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
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

4. Temporal Logics for Higher-Order Functional Programs based on Trace Semantics
with Yuki Satake

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]

Professional Activities