引用次数
引用: 928
H-指数: 17
I10-指数 : 23
出版物: 43
On-demand refinement of dependent types
Naoki Kobayashi , Hiroshi Unno
international symposium on functional and logic programming 81 -96
5
2008
Counterexample finding and abstraction refinment for automated Verification of higher-order tree transducers
Naoki Kobayashi , Hiroshi Unno , Yuma Matsumoto
Computer Software 32 ( 1) 161 -178
2015
Decision Tree Learning in CEGIS-Based Termination Analysis.
Ichiro Hasuo , Hiroshi Unno , Satoshi Kura
arXiv: Logic in Computer Science
8
2021
Predicate abstraction and CEGAR for higher-order model checking
Naoki Kobayashi , Ryosuke Sato , Hiroshi Unno
programming language design and implementation 46 ( 6) 222 -233
108
2011
Predicate Abstraction and CEGAR for Disproving Termination of Higher-Order Functional Programs
Takuya Kuwahara , Ryosuke Sato , Hiroshi Unno , Naoki Kobayashi
computer aided verification 287 -303
17
2015
Automata-Based Abstraction for Automated Verification of Higher-Order Tree-Processing Programs
Yuma Matsumoto , Naoki Kobayashi , Hiroshi Unno
asian symposium on programming languages and systems 295 -312
4
2015
Temporal Verification of Programs via First-Order Fixpoint Logic
Naoki Kobayashi , Takeshi Nishikawa , Atsushi Igarashi , Hiroshi Unno
static analysis symposium 413 -436
8
2019
Towards a scalable software model checker for higher-order programs
Ryosuke Sato , Hiroshi Unno , Naoki Kobayashi
partial evaluation and semantic-based program manipulation 53 -62
32
2013
Temporal verification of higher-order functional programs
Akihiro Murase , Tachio Terauchi , Naoki Kobayashi , Ryosuke Sato
symposium on principles of programming languages 51 ( 1) 57 -68
24
2016
Dependent type inference with interpolants
Hiroshi Unno , Naoki Kobayashi
principles and practice of declarative programming 277 -288
50
2009
Probabilistic Inference for Predicate Constraint Satisfaction.
Yuki Satake , Hiroshi Unno , Hinata Yanagi
national conference on artificial intelligence 34 ( 02) 1644 -1651
5
2020
Automating Induction for Solving Horn Clauses
Hiroshi Unno , Sho Torii , Hiroki Sakamoto
computer aided verification 571 -591
26
2017
Automating relatively complete verification of higher-order functional programs
Hiroshi Unno , Tachio Terauchi , Naoki Kobayashi
Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '13 48 ( 1) 75 -86
42
2013
Refinement Type Inference via Horn Constraint Optimization
Kodai Hashimoto , Hiroshi Unno
static analysis symposium 199 -216
11
2015
Automatic Termination Verification for Higher-Order Functional Programs
Takuya Kuwahara , Tachio Terauchi , Hiroshi Unno , Naoki Kobayashi
european symposium on programming 392 -411
29
2014
Higher-order multi-parameter tree transducers and recursion schemes for program verification
Naoki Kobayashi , Naoshi Tabuchi , Hiroshi Unno
Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '10 45 ( 1) 495 -508
59
2010
A Fixpoint Logic and Dependent Effects for Temporal Property Verification
Yoji Nanjo , Hiroshi Unno , Eric Koskinen , Tachio Terauchi
logic in computer science 759 -768
9
2018
Relatively complete refinement type system for verification of higher-order non-deterministic programs
Hiroshi Unno , Yuki Satake , Tachio Terauchi
Proceedings of the ACM on Programming Languages 2 12
7
2017
Combining type-based analysis and model checking for finding counterexamples against non-interference
Hiroshi Unno , Naoki Kobayashi , Akinori Yonezawa
Proceedings of the 2006 workshop on Programming languages and analysis for security - PLAS '06 17 -26
26
2006
Verification of tree-processing programs via higher-order model checking
Hiroshi Unno , Naoshi Tabuchi , Naoki Kobayashi
asian symposium on programming languages and systems 312 -327
17
2010