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

海野 広志

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

Unno, Hiroshi

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

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

オープンアクセス版の論文は「つくばリポジトリ」で読むことができます。
  1. 1. Higher-Order Model Checking of Effect-Handling Programs with Answer-Type Modification Taro Sekiyama; Hiroshi Unno
      Proceedings of the ACM on Programming Languages 8: 2662 - 2691 (2024) Semantic Scholar
  2. 2. Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System Satoshi Kura; Hiroshi Unno
      Proceedings of the ACM on Programming Languages 8: 973 - 1002 (2024)
  3. 3. Inductive Approach to Spacer Takeshi Tsukada; Hiroshi Unno
      Proceedings of the ACM on Programming Languages 8: 1979 - 2002 (2024) Semantic Scholar
  4. 4. Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers Fuga Kawamata; Hiroshi Unno; Taro Sekiyama; Tachio Terauchi
      Proceedings of the ACM on Programming Languages 8: 115 - 147 (2024) Semantic Scholar
  5. 5. Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification Hiroshi Unno; Tachio Terauchi; Yu Gu; Eric Koskinen
      Proceedings of the ACM on Programming Languages 7: 2111 - 2140 (2023) Semantic Scholar
  6. 6. Optimal CHC Solving via Termination Proofs. Yu Gu; Takeshi Tsukada; Hiroshi Unno 0001
      Proc. ACM Program. Lang. 7: 604 - 631 (2023) Semantic Scholar
  7. 7. Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations. Taro Sekiyama; Hiroshi Unno 0001
      Proc. ACM Program. Lang. 7: 2079 - 2110 (2023) Semantic Scholar
  8. 8. Software model-checking as cyclic-proof search Takeshi Tsukada; Hiroshi Unno
      Proceedings of the ACM on Programming Languages 6: 1 - 29 (2022) Semantic Scholar
  9. 9. Decision Tree Learning in CEGIS-Based Termination Analysis Satoshi Kura; Hiroshi Unno; Ichiro Hasuo
      Computer Aided Verification 75 - 98 (2021) Semantic Scholar
  10. 10. Constraint-Based Relational Verification Hiroshi Unno; Tachio Terauchi; Eric Koskinen
      Computer Aided Verification 742 - 766 (2021) Semantic Scholar
  11. 11. Toward Neural-Network-Guided Program Synthesis and Verification. Naoki Kobayashi 0001; Taro Sekiyama; Issei Sato; Hiroshi Unno 0001
      Static Analysis - 28th International Symposium(SAS) 236 - 260 (2021) Semantic Scholar
  12. 12. Decision Tree Learning in CEGIS-Based Termination Analysis. Satoshi Kura; Hiroshi Unno 0001; Ichiro Hasuo
      CoRR abs/2104.11463: (2021)
  13. 13. Enhancing Loop-Invariant Synthesis via Reinforcement Learning. Takeshi Tsukada; Hiroshi Unno 0001; Taro Sekiyama; Kohei Suenaga
      CoRR abs/2107.09766: (2021)
  14. 14. Toward Neural-Network-Guided Program Synthesis and Verification. Naoki Kobayashi 0001; Taro Sekiyama; Issei Sato; Hiroshi Unno 0001
      CoRR abs/2103.09414: (2021)
  15. 15. Probabilistic Inference for Predicate Constraint Satisfaction Yuki Satake; Hiroshi Unno; Hinata Yanagi
      Proceedings of AAAI 2020 (2020)
  16. 16. Failure of Cut-Elimination in Cyclic Proofs of Separation Logic KIMURA Daisuke; NAKAZAWA Koji; TERAUCHI Tachio; UNNO Hiroshi
      Computer Software 37: 1_39 - 1_52 (2020) Semantic Scholar
  17. 17. 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 - 436 (2019) Semantic Scholar
  18. 18. 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
  19. 19. 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
  20. 20. 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
1 2 3

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

  1. 1. Automating Relational Verification of Infinite-State Programs
    25th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2024) 2024年1月16日 招待有り
  2. 2. Constraint-based Relational Verification
    38th International Conference on Mathematical Foundations of Programming Semantics 2022年7月13日 招待有り
  3. 3. Horn Clauses and Beyond for Relational and Temporal Program Verification 海野 広志
    The 5th Workshop on Horn Clauses for Verification and Synthesis 2018年7月13日 招待有り
  4. 4. 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日 招待有り
  5. 5. Higher-order Program Verification as Refinement Type Inference 海野 広志
    The 3rd Workshop on Higher-Order Program Analysis (HOPA 2015) 2015年7月4日 招待有り

 295 total views