Follow
Hiroshi Unno
Title
Cited by
Cited by
Year
Predicate abstraction and CEGAR for higher-order model checking
N Kobayashi, R Sato, H Unno
Proceedings of the 32nd ACM SIGPLAN conference on Programming language …, 2011
1622011
Higher-order multi-parameter tree transducers and recursion schemes for program verification
N Kobayashi, N Tabuchi, H Unno
ACM Sigplan Notices 45 (1), 495-508, 2010
972010
Dependent type inference with interpolants
H Unno, N Kobayashi
Proceedings of the 11th ACM SIGPLAN conference on Principles and practice of …, 2009
762009
Automating relatively complete verification of higher-order functional programs
H Unno, T Terauchi, N Kobayashi
Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of …, 2013
552013
Automating induction for solving horn clauses
H Unno, S Torii, H Sakamoto
Computer Aided Verification: 29th International Conference, CAV 2017 …, 2017
532017
Towards a scalable software model checker for higher-order programs
R Sato, H Unno, N Kobayashi
Proceedings of the ACM SIGPLAN 2013 workshop on Partial evaluation and …, 2013
522013
Automatic termination verification for higher-order functional programs
T Kuwahara, T Terauchi, H Unno, N Kobayashi
European Symposium on Programming Languages and Systems, 392-411, 2014
412014
Constraint-based relational verification
H Unno, T Terauchi, E Koskinen
International Conference on Computer Aided Verification, 742-766, 2021
392021
Temporal verification of higher-order functional programs
A Murase, T Terauchi, N Kobayashi, R Sato, H Unno
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of …, 2016
312016
Verification of tree-processing programs via higher-order model checking
H Unno, N Tabuchi, N Kobayashi
Programming Languages and Systems: 8th Asian Symposium, APLAS 2010, Shanghai …, 2010
262010
Temporal verification of programs via first-order fixpoint logic
N Kobayashi, T Nishikawa, A Igarashi, H Unno
International Static Analysis Symposium, 413-436, 2019
252019
A fixpoint logic and dependent effects for temporal property verification
Y Nanjo, H Unno, E Koskinen, T Terauchi
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer …, 2018
252018
Combining type-based analysis and model checking for finding counterexamples against non-interference
H Unno, N Kobayashi, A Yonezawa
Proceedings of the 2006 workshop on Programming languages and analysis for …, 2006
252006
Relatively complete refinement type system for verification of higher-order non-deterministic programs
H Unno, Y Satake, T Terauchi
Proceedings of the ACM on Programming Languages 2 (POPL), 1-29, 2017
222017
Predicate abstraction and CEGAR for disproving termination of higher-order functional programs
T Kuwahara, R Sato, H Unno, N Kobayashi
Computer Aided Verification: 27th International Conference, CAV 2015, San …, 2015
212015
Probabilistic inference for predicate constraint satisfaction
Y Satake, H Unno, H Yanagi
Proceedings of the AAAI Conference on Artificial Intelligence 34 (02), 1644-1651, 2020
202020
Refinement type inference via horn constraint optimization
K Hashimoto, H Unno
Static Analysis: 22nd International Symposium, SAS 2015, Saint-Malo, France …, 2015
192015
Inferring simple solutions to recursion-free horn clauses via sampling
H Unno, T Terauchi
International Conference on Tools and Algorithms for the Construction and …, 2015
152015
Automata-based abstraction for automated verification of higher-order tree-processing programs
Y Matsumoto, N Kobayashi, H Unno
Programming Languages and Systems: 13th Asian Symposium, APLAS 2015, Pohang …, 2015
132015
Failure of cut-elimination in cyclic proofs of separation logic
D Kimura, K Nakazawa, T Terauchi, H Unno
コンピュータ ソフトウェア 37 (1), 1_39-1_52, 2020
112020
The system can't perform the operation now. Try again later.
Articles 1–20