ホーム > 海野広志/ Unno, Hiroshi

海野広志

ALUMNI 2025年11月現在、筑波大学が主たる所属機関ではありません

Unno, Hiroshi

東北大学 , 電気通信研究所 , 教授
Tohoku University , Research Institute of Electrical Communication

http://www.cs.tsukuba.ac.jp/~uhiro/

オープンアクセス版の論文は「つくばリポジトリ」で読むことができます。

21. Failure of Cut-Elimination in Cyclic Proofs of Separation Logic KIMURA Daisuke; NAKAZAWA Koji; TERAUCHI Tachio; UNNO Hiroshi
Computer Software 37: 1_39 (2020) Semantic Scholar
22. Temporal Verification of Programs via First-Order Fixpoint Logic Naoki Kobayashi; Takeshi Nishikawa; Atsushi Igarashi; Hiroshi Unno
Proceedings of SAS 2019 Springer LNCS 11822: 413 (2019) Semantic Scholar
23. Relatively complete refinement type system for verification of higher-order non-deterministic programs Hiroshi Unno; Yuki Satake; Tachio Terauchi
PACMPL 2: 12:1 (2018) Semantic Scholar
24. Propositional Dynamic Logic for Higher-Order Functional Programs Yuki Satake; Hiroshi Unno
Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I 105 (2018) Semantic Scholar
25. A Fixpoint Logic and Dependent Effects for Temporal Property Verification Yoji Nanjo; Hiroshi Unno; Eric Koskinen; Tachio Terauchi
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018 759 (2018) Semantic Scholar
26. Automating induction for solving horn clauses Hiroshi Unno; Sho Torii; Hiroki Sakamoto
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 10427: 571 - 591 (2017) Semantic Scholar
27. Automating induction for solving horn clauses Hiroshi Unno; Sho Torii; Hiroki Sakamoto
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 10427: 571 (2017) Semantic Scholar
28. Temporal verification of higher-order functional programs Akihiro Murase; Tachio Terauchi; Naoki Kobayashi; Ryosuke SatoHiroshi Unno
ACM SIGPLAN Notices 51: 57 - 68 (2016) Semantic Scholar
29. Temporal verification of higher-order functional programs Akihiro Murase; Tachio Terauchi; Naoki Kobayashi; Ryosuke SatoHiroshi Unno
Conference Record of the Annual ACM Symposium on Principles of Programming Languages 20-22-: 57 - 68 (2016) Semantic Scholar
30. Temporal verification of higher-order functional programs Akihiro Murase; Tachio Terauchi; Naoki Kobayashi; Ryosuke SatoHiroshi Unno
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016 57 (2016) Semantic Scholar
31. Verification of tree-processing programs via higher-order mode checking Hiroshi Unno; Naoshi Tabuchi; Naoki Kobayashi
MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE 25: 841 (2015) Semantic Scholar
32. Counterexample finding and abstraction refinment for automated Verification of higher-order tree transducers Yuma Matsumoto; Naoki Kobayashi; Hiroshi Unno
Computer Software 32: 161 (2015)
33. Relaxed Stratification: A New Approach to Practical Complete Predicate Refinement Tachio Terauchi; Hiroshi Unno
PROGRAMMING LANGUAGES AND SYSTEMS 9032: 610 (2015) Semantic Scholar
34. Inferring simple solutions to recursion-free horn clauses via sampling Hiroshi Unno; Tachio Terauchi
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 9035: 149 (2015) Semantic Scholar
35. Refinement Type Inference via Horn Constraint Optimization Kodai Hashimoto; Hiroshi Unno
STATIC ANALYSIS (SAS 2015) 9291: 199 (2015) Semantic Scholar
36. Predicate abstraction and CEGAR for disproving termination of Higher-Order functional programs Takuya Kuwahara; Ryosuke Sato; Hiroshi Unno; Naoki Kobayashi
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 9207: 287 (2015) Semantic Scholar
37. Automata-Based Abstraction for Automated Verification of Higher-Order Tree-Processing Programs Yuma Matsumoto; Naoki Kobayashi; Hiroshi Unno
PROGRAMMING LANGUAGES AND SYSTEMS, APLAS 2015 9458: 295 (2015) Semantic Scholar
38. Automatic Termination Verification for Higher-Order Functional Programs Takuya Kuwahara; Tachio Terauchi; Hiroshi Unno; Naoki Kobayashi
PROGRAMMING LANGUAGES AND SYSTEMS 8410: 392 (2014) Semantic Scholar
39. Automating relatively complete verification of higher-order functional programs Hiroshi Unno; Tachio Terauchi; Naoki Kobayashi
Conference Record of the Annual ACM Symposium on Principles of Programming Languages 75 (2013) Semantic Scholar
40. Towards a scalable software model checker for higher-order programs Ryosuke Sato; Hiroshi Unno; Naoki Kobayashi
PEPM 2013 - Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, Co-located with POPL 2013 53 (2013) Semantic Scholar

« 1 2 3 »

書籍等出版物情報はまだありません。

1. Software Verification via Fixed-Point Logics: Constraint Solving, Cyclic-Proof Search, and Strategy Synthesis
EPIT 2025 : École de Printemps d'Informatique Théorique 2025 2025年5月22日招待有り
2. Refinement Types and Higher-Order Model Checking for Algebraic Effects and Handlers
“CHoCoLa” meetings Curry-Howard: Logic and Computation 2025年5月15日招待有り
3. Automating Relational Verification of Infinite-State Programs
25th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2024) 2024年1月16日招待有り
4. Constraint-based Relational Verification
38th International Conference on Mathematical Foundations of Programming Semantics 2022年7月13日招待有り
5. Horn Clauses and Beyond for Relational and Temporal Program Verification 海野広志
The 5th Workshop on Horn Clauses for Verification and Synthesis 2018年7月13日招待有り
6. Tutorial: Applications of Higher-order Model Checking to Program Verification 海野広志
Workshop on Higher-Order Model Checking (HOMC) + Communicating, Distributed and Parameterised Systems (CDPS), 2016年9月20日招待有り
7. Higher-order Program Verification as Refinement Type Inference 海野広志
The 3rd Workshop on Higher-Order Program Analysis (HOPA 2015) 2015年7月4日招待有り