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

海野広志

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

Unno, Hiroshi

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

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

21. Decision Tree Learning in CEGIS-Based Termination Analysis Satoshi Kura; Hiroshi Unno; Ichiro Hasuo
Computer Aided Verification 75 (2021) Semantic Scholar
22. Constraint-Based Relational Verification Hiroshi Unno; Tachio Terauchi; Eric Koskinen
Computer Aided Verification 742 (2021) Semantic Scholar
23. Toward Neural-Network-Guided Program Synthesis and Verification. Naoki Kobayashi 0001; Taro Sekiyama; Issei Sato; Hiroshi Unno 0001
CoRR abs/2103.09414: (2021)
24. Enhancing Loop-Invariant Synthesis via Reinforcement Learning. Takeshi Tsukada; Hiroshi Unno 0001; Taro Sekiyama; Kohei Suenaga
CoRR abs/2107.09766: (2021)
25. Probabilistic Inference for Predicate Constraint Satisfaction Yuki Satake; Hiroshi Unno; Hinata Yanagi
Proceedings of the AAAI Conference on Artificial Intelligence 34: 1644 (2020)
26. 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
27. 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
28. 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
29. 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
30. 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
31. 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
32. 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
33. 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
34. 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
35. 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
36. 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
37. Counterexample finding and abstraction refinment for automated Verification of higher-order tree transducers Yuma Matsumoto; Naoki Kobayashi; Hiroshi Unno
Computer Software 32: 161 (2015)
38. Relaxed Stratification: A New Approach to Practical Complete Predicate Refinement Tachio Terauchi; Hiroshi Unno
PROGRAMMING LANGUAGES AND SYSTEMS 9032: 610 (2015) Semantic Scholar
39. 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
40. Refinement Type Inference via Horn Constraint Optimization Kodai Hashimoto; Hiroshi Unno
STATIC ANALYSIS (SAS 2015) 9291: 199 (2015) Semantic Scholar

« 1 2 3 »

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

1. Fixpoint Logics and Their Applications to Software Verification
IEEE International Symposium on Multiple-Valued Logic (ISMVL 2026) 2026年5月20日招待有り
2. 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日招待有り
3. Refinement Types and Higher-Order Model Checking for Algebraic Effects and Handlers
“CHoCoLa” meetings Curry-Howard: Logic and Computation 2025年5月15日招待有り
4. Automating Relational Verification of Infinite-State Programs
25th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2024) 2024年1月16日招待有り
5. Constraint-based Relational Verification
38th International Conference on Mathematical Foundations of Programming Semantics 2022年7月13日招待有り
6. Horn Clauses and Beyond for Relational and Temporal Program Verification 海野広志
The 5th Workshop on Horn Clauses for Verification and Synthesis 2018年7月13日招待有り
7. 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日招待有り
8. Higher-order Program Verification as Refinement Type Inference 海野広志
The 3rd Workshop on Higher-Order Program Analysis (HOPA 2015) 2015年7月4日招待有り