Hiroshi Unno

Publication Activity (10 Years)

Years Active: 2006-2024
Publications (10 Years): 26

Top Topics

Functional Programs

Top Venues

Proc. ACM Program. Lang.

Publications

Takeshi Tsukada, Hiroshi Unno
Inductive Approach to Spacer. Proc. ACM Program. Lang. 8 (PLDI) (2024)
Fuga Kawamata, Hiroshi Unno, Taro Sekiyama, Tachio Terauchi
Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers. Proc. ACM Program. Lang. 8 (POPL) (2024)
Satoshi Kura, Hiroshi Unno
Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System. CoRR (2024)
Hiroshi Unno, Tachio Terauchi, Yu Gu, Eric Koskinen
Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification. Proc. ACM Program. Lang. 7 (POPL) (2023)
Taro Sekiyama, Hiroshi Unno
Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations. Proc. ACM Program. Lang. 7 (POPL) (2023)
Yu Gu, Takeshi Tsukada, Hiroshi Unno
Optimal CHC Solving via Termination Proofs. Proc. ACM Program. Lang. 7 (POPL) (2023)
Fuga Kawamata, Hiroshi Unno, Taro Sekiyama, Tachio Terauchi
Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers. CoRR (2023)
Taro Sekiyama, Hiroshi Unno
Temporal Verification with Answer-Effect Modification. CoRR (2022)
Takeshi Tsukada, Hiroshi Unno
Software model-checking as cyclic-proof search. Proc. ACM Program. Lang. 6 (POPL) (2022)
Hiroshi Unno, Tachio Terauchi, Eric Koskinen
Constraint-based Relational Verification. CoRR (2021)
Naoki Kobayashi, Taro Sekiyama, Issei Sato, Hiroshi Unno
Toward Neural-Network-Guided Program Synthesis and Verification. SAS (2021)
Takeshi Tsukada, Hiroshi Unno
Software Model-Checking as Cyclic-Proof Search. CoRR (2021)
Hiroshi Unno, Tachio Terauchi, Eric Koskinen
Constraint-Based Relational Verification. CAV (1) (2021)
Satoshi Kura, Hiroshi Unno, Ichiro Hasuo
Decision Tree Learning in CEGIS-Based Termination Analysis. CoRR (2021)
Takeshi Tsukada, Hiroshi Unno, Taro Sekiyama, Kohei Suenaga
Enhancing Loop-Invariant Synthesis via Reinforcement Learning. CoRR (2021)
Naoki Kobayashi, Taro Sekiyama, Issei Sato, Hiroshi Unno
Toward Neural-Network-Guided Program Synthesis and Verification. CoRR (2021)
Satoshi Kura, Hiroshi Unno, Ichiro Hasuo
Decision Tree Learning in CEGIS-Based Termination Analysis. CAV (2) (2021)
Yuki Satake, Hiroshi Unno, Hinata Yanagi
Probabilistic Inference for Predicate Constraint Satisfaction. AAAI (2020)
Hiroshi Unno, Yuki Satake, Tachio Terauchi, Eric Koskinen
Program Verification via Predicate Constraint Satisfiability Modulo Theories. CoRR (2020)
Naoki Kobayashi, Takeshi Nishikawa, Atsushi Igarashi, Hiroshi Unno
Temporal Verification of Programs via First-Order Fixpoint Logic. SAS (2019)
Yoji Nanjo, Hiroshi Unno, Eric Koskinen, Tachio Terauchi
A Fixpoint Logic and Dependent Effects for Temporal Property Verification. LICS (2018)
Yuki Satake, Hiroshi Unno
Propositional Dynamic Logic for Higher-Order Functional Programs. CAV (1) (2018)
Hiroshi Unno, Yuki Satake, Tachio Terauchi
Relatively complete refinement type system for verification of higher-order non-deterministic programs. Proc. ACM Program. Lang. 2 (POPL) (2018)
Hiroshi Unno, Sho Torii, Hiroki Sakamoto
Automating Induction for Solving Horn Clauses. CAV (2) (2017)
Hiroshi Unno, Sho Torii
Automating Induction for Solving Horn Clauses. CoRR (2016)
Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, Hiroshi Unno
Temporal verification of higher-order functional programs. POPL (2016)
Hiroshi Unno, Tachio Terauchi
Inferring Simple Solutions to Recursion-Free Horn Clauses via Sampling. TACAS (2015)
Kodai Hashimoto, Hiroshi Unno
Refinement Type Inference via Horn Constraint Optimization. SAS (2015)
Takuya Kuwahara, Ryosuke Sato, Hiroshi Unno, Naoki Kobayashi
Predicate Abstraction and CEGAR for Disproving Termination of Higher-Order Functional Programs. CAV (2) (2015)
Hiroshi Unno, Naoshi Tabuchi, Naoki Kobayashi
Verification of tree-processing programs via higher-order mode checking. Math. Struct. Comput. Sci. 25 (4) (2015)
Tachio Terauchi, Hiroshi Unno
Relaxed Stratification: A New Approach to Practical Complete Predicate Refinement. ESOP (2015)
Yuma Matsumoto, Naoki Kobayashi, Hiroshi Unno
Automata-Based Abstraction for Automated Verification of Higher-Order Tree-Processing Programs. APLAS (2015)
Kodai Hashimoto, Hiroshi Unno
Refinement Type Inference via Horn Constraint Optimization. CoRR (2015)
Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno, Naoki Kobayashi
Automatic Termination Verification for Higher-Order Functional Programs. ESOP (2014)
Hiroshi Unno, Tachio Terauchi, Naoki Kobayashi
Automating relatively complete verification of higher-order functional programs. POPL (2013)
Ryosuke Sato, Hiroshi Unno, Naoki Kobayashi
Towards a scalable software model checker for higher-order programs. PEPM (2013)
Naoki Kobayashi, Ryosuke Sato, Hiroshi Unno
Predicate abstraction and CEGAR for higher-order model checking. PLDI (2011)
Naoki Kobayashi, Naoshi Tabuchi, Hiroshi Unno
Higher-order multi-parameter tree transducers and recursion schemes for program verification. POPL (2010)
Hiroshi Unno, Naoshi Tabuchi, Naoki Kobayashi
Verification of Tree-Processing Programs via Higher-Order Model Checking. APLAS (2010)
Hiroshi Unno, Naoki Kobayashi
Dependent type inference with interpolants. PPDP (2009)
Hiroshi Unno, Naoki Kobayashi
On-Demand Refinement of Dependent Types. FLOPS (2008)
Hiroshi Unno, Naoki Kobayashi, Akinori Yonezawa
Combining type-based analysis and model checking for finding counterexamples against non-interference. PLAS (2006)