Hiroshi UNNO

Assistant 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

Professional Activities

Software

Refinement Caml: Refinement Type Checking and Inference System based on Horn Clause Solving [FLOPS 08] [PPDP 09] [POPL 13] [APLAS 14] [TACAS 15] [SAS 15] [preprint2] [preprint3]
with Kodai Hashimoto, Daisuke Okamoto, and Sho Torii
[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]
with Ryosuke Sato, Takuya Kuwahara, Naoki Kobayashi, and Tachio Terauchi
[slides PPTX] [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]
with Naoshi Tabuchi, Yuma Matsumoto, and Naoki Kobayashi
[web demo]

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

Publications

2016

Temporal Verification of Higher-order Functional Programs
with Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, and Ryosuke Sato
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
with Yuma Matsumoto and Naoki Kobayashi
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
with Kodai Hashimoto
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
with Takuya Kuwahara, Ryosuke Sato, 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
with 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
with 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. (acceptance rate 24%=36/147)
[short version PDF] [full version PDF] [slides PPTX] [experiment data]

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

Counterexample Finding and Abstraction Refinement for Automated Verification of Higher-Order Transducers
with Yuma Matsumoto and Naoki Kobayashi
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)
with Kodai Hashimoto
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
with Takuya Kuwahara, Tachio Terauchi, 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. (acceptance rate 25%=27/109)
[short version PDF] [full version PDF] [web demo]

2013

Automating Relatively Complete Verification of Higher-Order Functional Programs
with Tachio Terauchi and 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. (acceptance rate 18%=43/238)
[short version PDF] [full version PDF] [slides PPTX] [web demo]

Towards a Scalable Software Model Checker for Higher-Order Programs
with Ryosuke Sato 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)
with Ryosuke Sato 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
with Naoki Kobayashi and Ryosuke Sato
In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2011), pp.222-233, San Jose, USA, June, 2011. (acceptance rate 23%=55/236)
[short version PDF] [full version PDF] [web demo]

2010

Verification of Tree-Processing Programs via Higher-Order Model Checking
with 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. (acceptance rate 33%=23/70)
[short version PDF] [full version PDF] [web demo]

Resource Usage Verification for a Programming Language with Pointers
with Shinpei Ueno and Naoki Kobayashi
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
with Naoki Kobayashi and Naoshi Tabuchi
In Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2010), pp.495-507, Madrid, Spain, January, 2010. (acceptance rate 19%=39/207)
[short version PDF] [full version PDF]

2009

Dependent Type Inference with Interpolants
with 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
with 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. (acceptance rate 37%=22/59)
[short version PDF] [full version PDF]

2006

Combining Type-Based Analysis and Model Checking for Finding Counterexamples against Non-Interference
with 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. Automating Total Correctness Verification of Higher-Order Functional Programs with Algebraic Data Types
with Kodai Hashimoto and Sho Torii

2. Automating Induction for Solving Horn Clauses
with 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]