Details of the Researcher

PHOTO

Hiroshi Unno
Section
Research Institute of Electrical Communication
Job title
Professor
Degree
e-Rad No.
80569575

Professional Memberships 2

  • JAPAN SOCIETY FOR SOFTWARE SCIENCE AND TECHNOLOGY

  • ACM

Research Interests 5

  • automated theorem proving

  • model checking

  • type systems

  • formal verification

  • programming languages

Research Areas 2

  • Informatics / Software /

  • Informatics / Information theory /

Papers 48

  1. A Hierarchy of Supermartingales for ω-Regular Verification Peer-reviewed

    Satoshi Kura, Hiroshi Unno

    Proceedings of the ACM on Programming Languages　2026/06/08

    DOI： 10.1145/3808257 　

  2. Supermartingales for Unique Fixed Points: A Unified Approach to Lower Bound Verification Peer-reviewed

    Satoshi Kura, Hiroshi Unno, Takeshi Tsukada

    Proceedings of the ACM on Programming Languages　2026/06/08

    DOI： 10.1145/3808348 　

  3. A Category-Theoretic Framework for Dependent Effect Systems Peer-reviewed

    Satoshi Kura, Marco Gaboardi, Taro Sekiyama, Hiroshi Unno

    Lecture Notes in Computer Science　401-431　2026/04/10

    Publisher: Springer Nature Switzerland

    DOI： 10.1007/978-3-032-22720-1_15 　

    ISSN： 0302-9743

    eISSN： 1611-3349

  4. On Higher-Order Model Checking of Effectful Answer-Type-Polymorphic Programs Peer-reviewed

    Taro Sekiyama, Ugo Dal Lago, Hiroshi Unno

    Proceedings of the ACM on Programming Languages　9　(OOPSLA2)　3726-3754　2025/10/09

    DOI： 10.1145/3763184 　

    eISSN： 2475-1421

  5. Thrust: A Prophecy-Based Refinement Type System for Rust Peer-reviewed

    Hiromi Ogawa, Taro Sekiyama, Hiroshi Unno

    Proceedings of the ACM on Programming Languages　9　(PLDI)　2056-2080　2025/06/10

    Publisher: Association for Computing Machinery (ACM)

    DOI： 10.1145/3729333 　

    eISSN： 2475-1421

    More details Close

    We introduce Thrust, a new verification tool for ensuring functional correctness in Rust, distinguished by its strengths in automated verification, including the synthesis of inductive invariants for loops and recursive functions. Thrust is built on a novel dependent refinement type system for Rust and refinement type inference techniques based on Constrained Horn Clause (CHC) solvers. Leveraging advantages of the type system, Thrust also supports semi-automated verification utilizing user type annotations to complement CHC solvers in cases where automatic constraint solving is unsuccessful, as well as modular verification at the function and subexpression levels. Thrust also achieves precise verification, especially for programs involving pointer aliasing and borrowing, without sacrificing the benefits of automated verification, by incorporating the notion of prophecy into the refinement type system: it not only enables strong updates by leveraging the “aliasing XOR mutability” guarantee provided by Rust’s type system, but also achieves propagation of update information to the original owner upon mutable borrow release through the use of a prophecy variable. Incorporating prophecy into a refinement type system is itself challenging and requires certain tricks, as discussed in this paper, making a theoretical contribution and paving the way for further research into prophecy-based refinement type systems. While our type system addresses the challenge, we keep it simple for extensibility, specifically by delegating the guarantee of “aliasing XOR mutability,” and, more technically, the “well-borrowedness” of the program in the sense of the stacked borrows aliasing model, to Rust’s type system, allowing us to focus on reasoning about functional correctness and propagating update information through prophecy variables. Compared to RustHorn, another automated verification tool based on prophecy, our approach leverages the strengths of refinement types to support modular verification, higher-order functions, and refinement of data stored in algebraic data structures. We implemented Thrust, a refinement type inference tool as a plugin for the Rust compiler, and evaluated it using RustHorn benchmarks, as well as additional new benchmarks, including those that are beyond the capabilities of RustHorn and other semi-automated verification tools, obtaining promising results.

  6. Solving Higher-Order Quantified Boolean Satisfiability via Higher-Order Model Checking Peer-reviewed

    Hiroshi Unno, Takeshi Tsukada, Jie-Hong Roland Jiang

    Proceedings of the AAAI Conference on Artificial Intelligence　39　(11)　11372-11380　2025/04/11

    Publisher: Association for the Advancement of Artificial Intelligence (AAAI)

    DOI： 10.1609/aaai.v39i11.33237 　

    ISSN： 2159-5399

    eISSN： 2374-3468

    More details Close

    The satisfiability (SAT) problem of higher-order quantified Boolean formula (HOQBF) emerged as a natural generalization of SAT, quantified SAT, and second-order quantified SAT. It allows succinct encoding of k-EXPTIME problems beyond the reach of prior Boolean satisfiability formulations, but its application was hampered by the lack of solvers. In this paper, we present the first HOQBF solver that leverages techniques from the model-checking community. Our HOQBF solver is based on reduction to higher-order model checking, which is a generalization from model checking of while-programs to that of higher-order functional programs. The ability of a higher-order model checker to deal with higher-order functions in a program is used to reason about higher-order quantifiers in HOQBF.

  7. Towards neural-network-guided program synthesis and verification Invited Peer-reviewed

    Naoki Kobayashi, Taro Sekiyama, Issei Sato, Hiroshi Unno

    Formal Methods in System Design　2025/02/24

    Publisher: Springer Science and Business Media LLC

    DOI： 10.1007/s10703-024-00468-9 　

    ISSN： 0925-9856

    eISSN： 1572-8102

    More details Close

    Abstract We propose a novel framework of program and invariant synthesis called neural network-guided synthesis (NeuGuS). We first show that, by suitably designing and training neural networks, we can extract logical formulas over integers from the weights and biases of the trained neural networks. Based on the idea, we have implemented a tool to synthesize formulas from positive/negative examples and implication constraints, and obtained promising experimental results. We also discuss two applications of our synthesis method. One is the use of our tool for qualifier discovery in the framework of ICE-learning-based CHC solving, which can in turn be applied to program verification and inductive invariant synthesis. Another application is to a new program development framework called oracle-based programming, which is a neural-network-guided variation of Solar-Lezama’s program synthesis by sketching.

  8. Algebraic Temporal Effects: Temporal Verification of Recursively Typed Higher-Order Programs Peer-reviewed

    Taro Sekiyama, Hiroshi Unno

    Proceedings of the ACM on Programming Languages　9　(POPL)　2306-2336　2025/01/07

    Publisher: Association for Computing Machinery (ACM)

    DOI： 10.1145/3704914 　

    eISSN： 2475-1421

    More details Close

    We present a general form of temporal effects for recursive types. Temporal effects have been adopted by effect systems to verify both linear-time temporal safety and liveness properties of higher-order programs with recursive functions. A challenge in a generalization to recursive types is that recursive types can easily cause unstructured loops, which obscure the regularity of the infinite behavior of computation and make it harder to statically verify liveness properties. To solve this problem, we introduce temporal effects with a later modality, which enable us to capture the behavior of non-terminating programs by stratifying obscure loops caused by recursive types. While temporal effects in the prior work are based on certain concrete formal forms, such as logical formulas and automata-based lattices, our temporal effects, which we call algebraic temporal effects, are more abstract, axiomatizing temporal effects in an algebraic manner and clarifying the requirements for temporal effects that can reason about programs soundly. We formulate algebraic temporal effects, formalize an effect system built on top of them, and prove two kinds of soundness of the effect system: safety and liveness soundness. We also introduce two instances of algebraic temporal effects: one is temporal regular effects, which are based on ω-regular expressions, and the other is temporal fixpoint effects, which are based on a first-order fixpoint logic. Their usefulness is demonstrated via examples including concurrent and object-oriented programs.

  9. A Primal-Dual Perspective on Program Verification Algorithms Peer-reviewed

    Takeshi Tsukada, Hiroshi Unno, Oded Padon, Sharon Shoham

    Proceedings of the ACM on Programming Languages　9　(POPL)　2025-2056　2025/01/07

    Publisher: Association for Computing Machinery (ACM)

    DOI： 10.1145/3704904 　

    eISSN： 2475-1421

    More details Close

    Many algorithms in verification and automated reasoning leverage some form of duality between proofs and refutations or counterexamples. In most cases, duality is only used as an intuition that helps in understanding the algorithms and is not formalized. In other cases, duality is used explicitly, but in a specially tailored way that does not generalize to other problems. In this paper we propose a unified primal-dual framework for designing verification algorithms that leverage duality. To that end, we generalize the concept of a Lagrangian that is commonly used in linear programming and optimization to capture the domains considered in verification problems, which are usually discrete, e.g., powersets of states, predicates, ranking functions, etc. A Lagrangian then induces a primal problem and a dual problem. We devise an abstract primal-dual procedure that simultaneously searches for a primal solution and a dual solution, where the two searches guide each other. We provide sufficient conditions that ensure that the procedure makes progress under certain monotonicity assumptions on the Lagrangian. We show that many existing algorithms in program analysis, verification, and automated reasoning can be derived from our algorithmic framework with a suitable choice of Lagrangian. The Lagrangian-based formulation sheds new light on various characteristics of these algorithms, such as the ingredients they use to ensure monotonicity and guarantee progress. We further use our framework to develop a new validity checking algorithm for fixpoint logic over quantified linear arithmetic. Our prototype achieves promising results and in some cases solves instances that are not solved by state-of-the-art techniques.

  10. Higher-Order Model Checking of Effect-Handling Programs with Answer-Type Modification Peer-reviewed

    Taro Sekiyama, Hiroshi Unno

    Proceedings of the ACM on Programming Languages　8　(OOPSLA2)　2662-2691　2024/10/08

    Publisher: Association for Computing Machinery (ACM)

    DOI： 10.1145/3689805 　

    eISSN： 2475-1421

    More details Close

    Model checking is one of the successful program verification methodologies. Since the seminal work by Ong, the model checking of higher-order programs―called higher-order model checking, or HOMC for short―has gained attention. It is also crucial for making HOMC applicable to real-world software to address programs involving computational effects. Recently, Dal Lago and Ghyselen considered an extension of HOMC to algebraic effect handlers, which enable programming the semantics of effects. They showed a negative result for HOMC with algebraic effect handlers―it is undecidable. In this work, we explore a restriction on programs with algebraic effect handlers which ensures the decidability of HOMC while allowing implementations of various effects. We identify the crux of the undecidability as the use of an unbounded number of algebraic effect handlers being active at the same time. To prevent it, we introduce answer-type modification (ATM), which can bound the number of algebraic effect handlers that can be active at the same time. We prove that ATM can ensure the decidability of HOMC and show that it accommodates a wide range of effects. To evaluate our approach, we implemented an automated verifier EffCaml based on the presented techniques and confirmed that the program examples discussed in this paper can be automatically verified.

  11. Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System Peer-reviewed

    Satoshi Kura, Hiroshi Unno

    Proceedings of the ACM on Programming Languages　8　(ICFP)　973-1002　2024/08/15

    Publisher: Association for Computing Machinery (ACM)

    DOI： 10.1145/3674662 　

    eISSN： 2475-1421

    More details Close

    Verification of higher-order probabilistic programs is a challenging problem. We present a verification method that supports several quantitative properties of higher-order probabilistic programs. Usually, extending verification methods to handle the quantitative aspects of probabilistic programs often entails extensive modifications to existing tools, reducing compatibility with advanced techniques developed for qualitative verification. In contrast, our approach necessitates only small amounts of modification, facilitating the reuse of existing techniques and implementations. On the theoretical side, we propose a dependent refinement type system for a generalised higher-order fixed point logic (HFL). Combined with continuation-passing style encodings of properties into HFL, our dependent refinement type system enables reasoning about several quantitative properties, including weakest pre-expectations, expected costs, moments of cost, and conditional weakest pre-expectations for higher-order probabilistic programs with continuous distributions and conditioning. The soundness of our approach is proved in a general setting using a framework of categorical semantics so that we don’t have to repeat similar proofs for each individual problem. On the empirical side, we implement a type checker for our dependent refinement type system that reduces the problem of type checking to constraint solving. We introduce admissible predicate variables and integrable predicate variables to constrained Horn clauses (CHC) so that we can soundly reason about the least fixed points and samplings from probability distributions. Our implementation demonstrates that existing CHC solvers developed for non-probabilistic programs can be extended to a solver for the extended CHC with only small efforts. We also demonstrate the ability of our type checker to verify various concrete examples.

  12. Inductive Approach to Spacer Peer-reviewed

    Takeshi Tsukada, Hiroshi Unno

    Proceedings of the ACM on Programming Languages　8　(PLDI)　1979-2002　2024/06/20

    Publisher: Association for Computing Machinery (ACM)

    DOI： 10.1145/3656457 　

    eISSN： 2475-1421

    More details Close

    The constrained Horn clause satisfiability problem is at the core of many automated verification methods, and Spacer is one of the most efficient solvers of this problem. The standard description of Spacer is based on an abstract transition system, dividing the whole procedure into small rules. This division makes individual rules easier to understand but, conversely, makes it difficult to discuss the procedure as a whole. As evidence of the difficulty in understanding the whole procedure, we point out that the claimed refutational completeness actually fails for several reasons, some of which were not present in the original version and subsequently added. It is also difficult to grasp the differences between Spacer and another procedure, such as GPDR. This paper aims to provide a better understanding of Spacer by developing a Spacer-like procedure defined by structural induction. We first formulate the problem to be solved inductively, then give its naïve solver and transform it to obtain a Spacer-like procedure. Interestingly, our inductive approach almost unifies Spacer and GPDR, which differ in only one respect in our understanding. To demonstrate the usefulness of our inductive approach in understanding Spacer, we examine Spacer variants in the literature in terms of inductive procedures and discuss why they are not refutationally complete and how to fix them. We also implemented the proposed procedure and evaluated it experimentally.

  13. Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers Peer-reviewed

    Fuga Kawamata, Hiroshi Unno, Taro Sekiyama, Tachio Terauchi

    Proceedings of the ACM on Programming Languages　8　(POPL)　115-147　2024/01/05

    Publisher: Association for Computing Machinery (ACM)

    DOI： 10.1145/3633280 　

    eISSN： 2475-1421

    More details Close

    Algebraic effects and handlers are a mechanism to structure programs with computational effects in a modular way. They are recently gaining popularity and being adopted in practical languages, such as OCaml. Meanwhile, there has been substantial progress in program verification via refinement type systems . While a variety of refinement type systems have been proposed, thus far there has not been a satisfactory refinement type system for algebraic effects and handlers. In this paper, we fill the void by proposing a novel refinement type system for languages with algebraic effects and handlers. The expressivity and usefulness of algebraic effects and handlers come from their ability to manipulate delimited continuations , but delimited continuations also complicate programs’ control flow and make their verification harder. To address the complexity, we introduce a novel concept that we call answer refinement modification (ARM for short), which allows the refinement type system to precisely track what effects occur and in what order when a program is executed, and reflect such information as modifications to the refinements in the types of delimited continuations. We formalize our type system that supports ARM (as well as answer type modification, or ATM) and prove its soundness. Additionally, as a proof of concept, we have extended the refinement type system to a subset of OCaml 5 which comes with a built-in support for effect handlers, implemented a type checking and inference algorithm for the extension, and evaluated it on a number of benchmark programs that use algebraic effects and handlers. The evaluation demonstrates that ARM is conceptually simple and practically useful. Finally, a natural alternative to directly reasoning about a program with delimited continuations is to apply a continuation passing style (CPS) transformation that transforms the program to a pure program without delimited continuations. We investigate this alternative in the paper, and show that the approach is indeed possible by proposing a novel CPS transformation for algebraic effects and handlers that enjoys bidirectional (refinement-)type-preservation. We show that there are pros and cons with this approach, namely, while one can use an existing refinement type checking and inference algorithm that can only (directly) handle pure programs, there are issues such as needing type annotations in source programs and making the inferred types less informative to a user.

  14. Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification Peer-reviewed

    Hiroshi Unno, Tachio Terauchi, Yu Gu, Eric Koskinen

    Proceedings of the ACM on Programming Languages　7　(POPL)　2111-2140　2023/01/09

    Publisher: Association for Computing Machinery (ACM)

    DOI： 10.1145/3571265 　

    eISSN： 2475-1421

    More details Close

    We present a novel approach to deciding the validity of formulas in first-order fixpoint logic with background theories and arbitrarily nested inductive and co-inductive predicates defining least and greatest fixpoints. Our approach is constraint-based, and reduces the validity checking problem of the given first-order-fixpoint logic formula (formally, an instance in a language called µCLP) to a constraint satisfaction problem for a recently introduced predicate constraint language. Coupled with an existing sound-and-relatively-complete solver for the constraint language, this novel reduction alone already gives a sound and relatively complete method for deciding µCLP validity, but we further improve it to a novel modular primal-dual method. The key observations are (1) µCLP is closed under complement such that each (co-)inductive predicate in the original primal instance has a corresponding (co-)inductive predicate representing its complement in the dual instance obtained by taking the standard De Morgan’s dual of the primal instance, and (2) partial solutions for (co-)inductive predicates synthesized during the constraint solving process of the primal side can be used as sound upper-bounds of the corresponding (co-)inductive predicates in the dual side, and vice versa. By solving the primal and dual problems in parallel and exchanging each others’ partial solutions as sound bounds, the two processes mutually reduce each others’ solution spaces, thus enabling rapid convergence. The approach is also modular in that the bounds are synthesized and exchanged at granularity of individual (co-)inductive predicates. We demonstrate the utility of our novel fixpoint logic solving by encoding a wide variety of temporal verification problems in µCLP, including termination/non-termination, LTL, CTL, and even the full modal µ-calculus model checking of infinite state programs. The encodings exploit the modularity in both the program and the property by expressing each loops and (recursive) functions in the program and sub-formulas of the property as individual (possibly nested) (co-)inductive predicates. Together with our novel modular primal-dual µCLP solving, we obtain a novel approach to efficiently solving a wide range of temporal verification problems.

  15. Optimal CHC Solving via Termination Proofs. Peer-reviewed

    Yu Gu, Takeshi Tsukada, Hiroshi Unno 0001

    Proc. ACM Program. Lang.　7　(POPL)　604-631　2023/01

    DOI： 10.1145/3571214 　

  16. Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations. Peer-reviewed

    Taro Sekiyama, Hiroshi Unno 0001

    Proc. ACM Program. Lang.　7　(POPL)　2079-2110　2023/01

    DOI： 10.1145/3571264 　

  17. Software model-checking as cyclic-proof search Peer-reviewed

    Takeshi Tsukada, Hiroshi Unno

    Proceedings of the ACM on Programming Languages　6　(POPL)　1-29　2022/01/16

    Publisher: Association for Computing Machinery (ACM)

    DOI： 10.1145/3498725 　

    eISSN： 2475-1421

    More details Close

    This paper shows that a variety of software model-checking algorithms can be seen as proof-search strategies for a non-standard proof system, known as a <italic>cyclic proof system</italic> . Our use of the cyclic proof system as a logical foundation of software model checking enables us to compare different algorithms, to reconstruct well-known algorithms from a few simple principles, and to obtain soundness proofs of algorithms for free. Among others, we show the significance of a heuristics based on a notion that we call <italic>maximal conservativity</italic> ; this explains the cores of important algorithms such as property-directed reachability (PDR) and reveals a surprising connection to an efficient solver of games over infinite graphs that was not regarded as a kind of PDR.

  18. Toward Neural-Network-Guided Program Synthesis and Verification. Peer-reviewed

    Naoki Kobayashi 0001, Taro Sekiyama, Issei Sato, Hiroshi Unno 0001

    Static Analysis - 28th International Symposium(SAS)　236-260　2021

    Publisher: Springer

    DOI： 10.1007/978-3-030-88806-0_12 　

  19. Constraint-Based Relational Verification Peer-reviewed

    Hiroshi Unno, Tachio Terauchi, Eric Koskinen

    Computer Aided Verification　742-766　2021

    Publisher: Springer International Publishing

    DOI： 10.1007/978-3-030-81685-8_35 　

    ISSN： 0302-9743

    eISSN： 1611-3349

    More details Close

    <title>Abstract</title>In recent years they have been numerous works that aim to automate relational verification. Meanwhile, although Constrained Horn Clauses (<inline-formula><alternatives><tex-math>$$\mathrm {CHCs}$$</tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>CHCs</mml:mi> </mml:math></alternatives></inline-formula>) empower a wide range of verification techniques and tools, they lack the ability to express hyperproperties beyond <italic>k</italic>-safety such as generalized non-interference and co-termination. This paper describes a novel and fully automated constraint-based approach to relational verification. We first introduce a new class of predicate Constraint Satisfaction Problems called <inline-formula><alternatives><tex-math>$$\mathrm {pfwCSP}$$</tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>pfwCSP</mml:mi> </mml:math></alternatives></inline-formula> where constraints are represented as clauses modulo first-order theories over predicate variables of three kinds: ordinary, well-founded, or functional. This generalization over <inline-formula><alternatives><tex-math>$$\mathrm {CHCs}$$</tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>CHCs</mml:mi> </mml:math></alternatives></inline-formula> permits arbitrary (i.e., possibly non-Horn) clauses, well-foundedness constraints, functionality constraints, and is capable of expressing these relational verification problems. Our approach enables us to express and automatically verify problem instances that require non-trivial (i.e., non-sequential and non-lock-step) self-composition by automatically inferring appropriate <italic>schedulers</italic> (or <italic>alignment</italic>) that dictate when and which program copies move. To solve problems in this new language, we present a constraint solving method for <inline-formula><alternatives><tex-math>$$\mathrm {pfwCSP}$$</tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>pfwCSP</mml:mi> </mml:math></alternatives></inline-formula> based on <italic>stratified</italic> CounterExample-Guided Inductive Synthesis (CEGIS) of ordinary, well-founded, and functional predicates. We have implemented the proposed framework and obtained promising results on diverse relational verification problems that are beyond the scope of the previous verification frameworks.

  20. Decision Tree Learning in CEGIS-Based Termination Analysis Peer-reviewed

    Satoshi Kura, Hiroshi Unno, Ichiro Hasuo

    Computer Aided Verification　75-98　2021

    Publisher: Springer International Publishing

    DOI： 10.1007/978-3-030-81688-9_4 　

    ISSN： 0302-9743

    eISSN： 1611-3349

    More details Close

    <title>Abstract</title>We present a novel decision tree-based synthesis algorithm of ranking functions for verifying program termination. Our algorithm is integrated into the workflow of CounterExample Guided Inductive Synthesis (CEGIS). CEGIS is an iterative learning model where, at each iteration, (1) a synthesizer synthesizes a candidate solution from the current examples, and (2) a validator accepts the candidate solution if it is correct, or rejects it providing counterexamples as part of the next examples. Our main novelty is in the design of a synthesizer: building on top of a usual decision tree learning algorithm, our algorithm detects <italic>cycles</italic> in a set of example transitions and uses them for refining decision trees. We have implemented the proposed method and obtained promising experimental results on existing benchmark sets of (non-)termination verification problems that require synthesis of piecewise-defined lexicographic affine ranking functions.

  21. Probabilistic Inference for Predicate Constraint Satisfaction

    Yuki Satake, Hiroshi Unno, Hinata Yanagi

    Proceedings of the AAAI Conference on Artificial Intelligence　34　(02)　1644-1651　2020/04/03

    Publisher: Association for the Advancement of Artificial Intelligence (AAAI)

    DOI： 10.1609/aaai.v34i02.5526 　

    ISSN： 2159-5399

    eISSN： 2374-3468

    More details Close

    In this paper, we present a novel constraint solving method for a class of predicate Constraint Satisfaction Problems (pCSP) where each constraint is represented by an arbitrary clause of first-order predicate logic over predicate variables. The class of pCSP properly subsumes the well-studied class of Constrained Horn Clauses (CHCs) where each constraint is restricted to a Horn clause. The class of CHCs has been widely applied to verification of linear-time safety properties of programs in different paradigms. In this paper, we show that pCSP further widens the applicability to verification of branching-time safety properties of programs that exhibit finitely-branching non-determinism. Solving pCSP (and CHCs) however is challenging because the search space of solutions is often very large (or unbounded), high-dimensional, and non-smooth. To address these challenges, our method naturally combines techniques studied separately in different literatures: counterexample guided inductive synthesis (CEGIS) and probabilistic inference in graphical models. We have implemented the presented method and obtained promising results on existing benchmarks as well as new ones that are beyond the scope of existing CHC solvers.

  22. Failure of Cut-Elimination in Cyclic Proofs of Separation Logic Invited Peer-reviewed

    KIMURA Daisuke, NAKAZAWA Koji, TERAUCHI Tachio, UNNO Hiroshi

    Computer Software　37　(1)　1_39-1_52　2020

    Publisher: Japan Society for Software Science and Technology

    DOI： 10.11309/jssst.37.1_39 　

    ISSN： 0289-6540

    More details Close

    <p>This paper studies the role of the cut rule in cyclic proof systems for separation logic. A cyclic proof system is a sequent-calculus style proof system for proving properties involving inductively defined predicates. Recently, there has been much interest in using cyclic proofs for proving properties described in separation logic with inductively defined predicates. In particular, for program verification, several theorem provers based on mechanical proof search procedures in cyclic proof systems for separation logic have been proposed. This paper shows that the cut-elimination property fails in cyclic proof systems for separation logic in several settings. We present two systems, one for sequents with single-antecedent and single-conclusion, and another for sequents with single-antecedent and multiple-conclusions. To show the cut-elimination failure, we present concrete and reasonably simple counter-example sequents which the systems can prove with cuts but not without cuts. This result suggests that the cut rule is important for a practical application of cyclic proofs to separation logic, since a naïve proof search procedure, which tries to find a cut-free proof, gives a limit to what one would be able to prove.</p>

  23. Temporal Verification of Programs via First-Order Fixpoint Logic Peer-reviewed

    Naoki Kobayashi, Takeshi Nishikawa, Atsushi Igarashi, Hiroshi Unno

    Proceedings of SAS 2019　Springer LNCS 11822　413-436　2019/10

    DOI： 10.1007/978-3-030-32304-2_20 　

  24. Relatively complete refinement type system for verification of higher-order non-deterministic programs Peer-reviewed

    Hiroshi Unno, Yuki Satake, Tachio Terauchi

    PACMPL　2　({POPL})　12:1-12:29　2018

    DOI： 10.1145/3158100 　

  25. Propositional Dynamic Logic for Higher-Order Functional Programs Peer-reviewed

    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

    DOI： 10.1007/978-3-319-96145-3_6 　

  26. A Fixpoint Logic and Dependent Effects for Temporal Property Verification Peer-reviewed

    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

    DOI： 10.1145/3209108.3209204 　

  27. Automating induction for solving horn clauses Peer-reviewed

    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

    Publisher: Springer Verlag

    DOI： 10.1007/978-3-319-63390-9_30 　

    ISSN： 1611-3349 0302-9743

  28. Temporal verification of higher-order functional programs Peer-reviewed

    Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, Hiroshi 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

    DOI： 10.1145/2837614.2837667 　

  29. Verification of tree-processing programs via higher-order mode checking Peer-reviewed

    Hiroshi Unno, Naoshi Tabuchi, Naoki Kobayashi

    MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE　25　(4)　841-866　2015/05

    DOI： 10.1017/S0960129513000054 　

    ISSN： 0960-1295

    eISSN： 1469-8072

  30. Counterexample finding and abstraction refinment for automated Verification of higher-order tree transducers

    Yuma Matsumoto, Naoki Kobayashi, Hiroshi Unno

    Computer Software　32　(1)　161-178　2015

    Publisher: Japan Society for Software Science and Technology

    ISSN： 0289-6540

  31. Relaxed Stratification: A New Approach to Practical Complete Predicate Refinement Peer-reviewed

    Tachio Terauchi, Hiroshi Unno

    PROGRAMMING LANGUAGES AND SYSTEMS　9032　610-633　2015

    DOI： 10.1007/978-3-662-46669-8_25 　

    ISSN： 0302-9743

  32. Inferring simple solutions to recursion-free horn clauses via sampling Peer-reviewed

    Hiroshi Unno, Tachio Terauchi

    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)　9035　149-163　2015

    Publisher: Springer Verlag

    DOI： 10.1007/978-3-662-46681-0_10 　

    ISSN： 1611-3349 0302-9743

  33. Refinement Type Inference via Horn Constraint Optimization Peer-reviewed

    Kodai Hashimoto, Hiroshi Unno

    STATIC ANALYSIS (SAS 2015)　9291　199-216　2015

    DOI： 10.1007/978-3-662-48288-9_12 　

    ISSN： 0302-9743

  34. Predicate abstraction and CEGAR for disproving termination of Higher-Order functional programs Peer-reviewed

    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-303　2015

    Publisher: Springer Verlag

    DOI： 10.1007/978-3-319-21668-3_17 　

    ISSN： 1611-3349 0302-9743

  35. Automata-Based Abstraction for Automated Verification of Higher-Order Tree-Processing Programs Peer-reviewed

    Yuma Matsumoto, Naoki Kobayashi, Hiroshi Unno

    PROGRAMMING LANGUAGES AND SYSTEMS, APLAS 2015　9458　295-312　2015

    DOI： 10.1007/978-3-319-26529-2_16 　

    ISSN： 0302-9743

  36. Automatic Termination Verification for Higher-Order Functional Programs Peer-reviewed

    Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno, Naoki Kobayashi

    PROGRAMMING LANGUAGES AND SYSTEMS　8410　392-411　2014

    DOI： 10.1007/978-3-642-54833-8_21 　

    ISSN： 0302-9743

  37. Automating relatively complete verification of higher-order functional programs Peer-reviewed

    Hiroshi Unno, Tachio Terauchi, Naoki Kobayashi

    Conference Record of the Annual ACM Symposium on Principles of Programming Languages　75-86　2013

    DOI： 10.1145/2429069.2429081 　

    ISSN： 0730-8566

  38. Towards a scalable software model checker for higher-order programs Peer-reviewed

    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-62　2013

    DOI： 10.1145/2426890.2426900 　

  39. Predicate Abstraction and CEGAR for Higher-Order Model Checking Peer-reviewed

    Naoki Kobayashi, Ryosuke Sato, Hiroshi Unno

    PLDI 11: PROCEEDINGS OF THE 2011 ACM CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION　222-233　2011

    DOI： 10.1145/1993498.1993525 　

  40. Higher-Order Multi-Parameter Tree Transducers and Recursion Schemes for Program Verification Peer-reviewed

    Naoki Kobayashi, Naoshi Tabuchi, Hiroshi Unno

    POPL'10: PROCEEDINGS OF THE 37TH ANNUAL ACM SIGPLAN-SIGACT SYMPOSIUM ON PRINCIPLES OF PROGRAMMING LANGUAGES　495-507　2010

    DOI： 10.1145/1706299.1706355 　

  41. Verification of Tree-Processing Programs via Higher-Order Model Checking Peer-reviewed

    Hiroshi Unno, Naoshi Tabuchi, Naoki Kobayashi

    PROGRAMMING LANGUAGES AND SYSTEMS　6461　312-327　2010

    DOI： 10.1007/978-3-642-17164-2_22 　

    ISSN： 0302-9743

  42. Dependent Type Inference with Interpolants Peer-reviewed

    Hiroshi Unno, Naoki Kobayashi

    PPDP&apos;09: PROCEEDINGS OF THE 11TH INTERNATIONAL ACM SIGPLAN SYMPOSIUM ON PRINCIPLES AND PRACTICE OF DECLARATIVE PROGRAMMING　277-288　2009

    DOI： 10.1145/1599410.1599445 　

  43. On-demand refinement of dependent types Peer-reviewed

    Hiroshi Unno, Naoki Kobayashi

    FUNCTIONAL AND LOGIC PROGRAMMING　4989　81-+　2008

    DOI： 10.1007/978-3-540-78969-7_8 　

    ISSN： 0302-9743

  44. Combining type-based analysis and model checking for finding counterexamples against non-interference Peer-reviewed

    Hiroshi Unno, Naoki Kobayashi, Akinori Yonezawa

    Proceedings of the 2006 Workshop on Programming Languages and Analysis for Security, PLAS 2006, Ottawa, Ontario, Canada, June 10, 2006　17　2006

    DOI： 10.1145/1134744.1134750 　

  45. Lagrangian-Based Duality for Quantified SMT Algorithms

    Ivana Bocevska, Takeshi Tsukada, Hiroshi Unno, Oded Padon, Sharon Shoham

    2026

    DOI： 10.1007/978-3-032-32526-6_4 　

  46. Enhancing Loop-Invariant Synthesis via Reinforcement Learning.

    Takeshi Tsukada, Hiroshi Unno 0001, Taro Sekiyama, Kohei Suenaga

    CoRR　abs/2107.09766　2021

  47. Toward Neural-Network-Guided Program Synthesis and Verification.

    Naoki Kobayashi 0001, Taro Sekiyama, Issei Sato, Hiroshi Unno 0001

    CoRR　abs/2103.09414　2021

  48. Automating Relatively Complete Verification of Higher-Order Functional Programs Peer-reviewed

    Hiroshi Unno, Tachio Terauchi, Naoki Kobayashi

    ACM SIGPLAN NOTICES　48　(1)　75-86　2013/01

    DOI： 10.1145/2480359.2429081 　

    ISSN： 0362-1340

Show all ︎Show first 5

Presentations 8

  1. Fixpoint Logics and Their Applications to Software Verification Invited

    Hiroshi Unno

    IEEE International Symposium on Multiple-Valued Logic (ISMVL 2026)　2026/05/20

  2. Software Verification via Fixed-Point Logics: Constraint Solving, Cyclic-Proof Search, and Strategy Synthesis Invited

    Hiroshi Unno

    EPIT 2025 : École de Printemps d'Informatique Théorique 2025　2025/05/22

  3. Refinement Types and Higher-Order Model Checking for Algebraic Effects and Handlers Invited

    Hiroshi Unno

    “CHoCoLa” meetings Curry-Howard: Logic and Computation　2025/05/15

  4. Automating Relational Verification of Infinite-State Programs Invited

    Hiroshi Unno

    25th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2024)　2024/01/16

  5. Constraint-based Relational Verification Invited

    Hiroshi Unno

    38th International Conference on Mathematical Foundations of Programming Semantics　2022/07/13

  6. Horn Clauses and Beyond for Relational and Temporal Program Verification International-presentation Invited

    Hiroshi Unno

    The 5th Workshop on Horn Clauses for Verification and Synthesis　2018/07/13

  7. Tutorial: Applications of Higher-order Model Checking to Program Verification International-presentation Invited

    Hiroshi Unno

    Workshop on Higher-Order Model Checking (HOMC) + Communicating, Distributed and Parameterised Systems (CDPS),　2016/09/20

  8. Higher-order Program Verification as Refinement Type Inference International-presentation Invited

    Hiroshi Unno

    The 3rd Work- shop on Higher-Order Program Analysis (HOPA 2015)　2015/07/04

Show all Show first 5

Research Projects 18

  1. プログラム検証技術の基礎付けと応用

    海野 広志

    Offer Organization: 日本学術振興会

    System: 科学研究費助成事業

    Category: 基盤研究(S)

    Institution: 東北大学

    2025/04/01 - 2030/03/31

  2. Scalable Automated Program Verification for Concurrent and Parallel Programs

    Offer Organization: Japan Society for the Promotion of Science

    System: Grants-in-Aid for Scientific Research

    Category: Grant-in-Aid for Scientific Research (A)

    Institution: National Institute of Informatics

    2024/04 - 2028/03

  3. Dependent refinement types and predicate constraints for program verification

    Offer Organization: Japan Society for the Promotion of Science

    System: Grants-in-Aid for Scientific Research

    Category: Grant-in-Aid for Scientific Research (B)

    Institution: Waseda University

    2024/04/01 - 2027/03/31

  4. 機械学習技術による高速な演繹的推論エンジンの開発

    塚田 武志, 末永 幸平, 海野 広志, 関山 太朗

    Offer Organization: 日本学術振興会

    System: 科学研究費助成事業

    Category: 基盤研究(B)

    Institution: 千葉大学

    2024/04/01 - 2027/03/31

  5. Dependent refinement types and predicate constraints for program verification

    Offer Organization: Japan Society for the Promotion of Science

    System: Grants-in-Aid for Scientific Research

    Category: Grant-in-Aid for Scientific Research (B)

    Institution: Waseda University

    2022/04/01 - 2027/03/31

  6. 機械学習技術による高速な演繹的推論エンジンの開発

    塚田 武志, 末永 幸平, 海野 広志, 関山 太朗

    Offer Organization: 日本学術振興会

    System: 科学研究費助成事業

    Category: 基盤研究(B)

    Institution: 千葉大学

    2022/04/01 - 2027/03/31

    More details Close

    SyGuS という競技会における Inv トラックで優勝できるレベルの高性能なソルバを作成することができた。これは当初の計画における最初のステップであり、これが目論見通り達成できたことになる。機械学習としては強化学習を用いており、素朴なアルゴリズムでも専門家が与えたヒューリスティクスや他の SyGuS の参加ソルバよりも高性能なソルバを作成することができ、さらに進んだアルゴリズムを使うことでさらに高性能なソルバを作ることができた。しかしながら SyGuS 競技会の内容が変更されたため、実際に競技会に参加して優勝することは叶わなかった。 この成果の意義は不変条件の発見というタスクにおいても機械学習技術が効果を発揮することを明らかにしたことにある。機械学習の演繹的推論への応用例は多いが、それらは不変条件の発見のような適切な論理式を発見するタスクを対象外または苦手とするか、あるいは適切な論理式の発見タスクを扱うが既存ソルバに比べて実行効率の面で劣っていた。不変条件の発見のようなタスクにおいても機械学習技術を援用することでソルバの効率を挙げられるということは、重要な発見である。 SyGuS に優勝するレベルのソルバができたことは重要な進展だが、一方でプログラム検証などへの応用を考えると、作成したソルバが完全に満足の行くものとまでは言えない。その理由は (1) SyGuS 競技会に参加していない非常に優秀なあるソルバと比べると必ずしも勝っているとは言えないこと、(2) SyGuS の Inv トラックの問題はある側面では比較的簡単な（正確にいうと未定述語が１つ）ものであり、応用法はこのクラスから外れる問題も多いこと、が挙げられる。

  7. Synthesis of High-Level Programs from Temporal and Relational Specifications

    Offer Organization: Japan Society for the Promotion of Science

    System: Grants-in-Aid for Scientific Research

    Category: Grant-in-Aid for Scientific Research (B)

    Institution: Tohoku University

    2024/04/01 - 2025/03/31

  8. Program Verification Techniques for the AI Era

    Offer Organization: Japan Society for the Promotion of Science

    System: Grants-in-Aid for Scientific Research Grant-in-Aid for Scientific Research (S)

    Category: Grant-in-Aid for Scientific Research (S)

    Institution: The University of Tokyo

    2020/08/31 - 2025/03/31

  9. Synthesis of High-Level Programs from Temporal and Relational Specifications

    Offer Organization: Japan Society for the Promotion of Science

    System: Grants-in-Aid for Scientific Research Grant-in-Aid for Scientific Research (B)

    Category: Grant-in-Aid for Scientific Research (B)

    Institution: University of Tsukuba

    2020/04/01 - 2025/03/31

  10. IoT システムのための形式検証手法の深化

    末永 幸平, 五十嵐 淳, 海野 広志

    Offer Organization: 日本学術振興会

    System: 科学研究費助成事業 基盤研究(B)

    Category: 基盤研究(B)

    Institution: 京都大学

    2019/04/01 - 2024/03/31

    More details Close

    本年は特に課題B（人間による自動検証支援手法）について，大きな進捗があった．人間により自動検証支援を行う当初の計画に関連する研究として，提案時に人間が行うことを予定していた自動検証手法への操作を機械学習を用いて行う手法を研究した．この手法は，CEGIS と呼ばれる検証手法において用いられているヒューリスティクスを強化学習によって自動的に学習する手法である．このヒューリスティクスは，従来は人手でアドホックにチューニングされていたが，これを自動的にチューニングし高性能なヒューリスティクスを得る手法を提案した． この手法を検証器 PCSat に実装し，自動検証分野の標準的なベンチマークである SyGuS-Comp によって評価した．評価にあたっては，現在このベンチマークで世界トップレベルのツールである CVC4 と比較した．その結果，強化学習により学習されたヒューリスティクスを用いる PCSat の性能は，CVC4 の性能を超えた．この結果は，強化学習により検証器のヒューリスティクスを改善する研究としては新規なものであり，その有用性が実験によって確かめられた点で意義深い．この成果を論文にまとめて投稿中である． ハイブリッドシステムの検証に関しては引き続き手法の検討を継続しており，今年度の課題Bの成果の適用を視野に入れつつ研究を行っている．

  11. Verification of high-level programs containing mutable higher-order recursive data structures Competitive

    Tachio Terauchi

    Offer Organization: Japan Society for the Promotion of Science

    System: Grant-in-Aid for Scientific Research (B)

    Category: Grant-in-Aid for Scientific Research (B)

    Institution: Waseda University

    2017/04 - 2022/03

    More details Close

    We have achieved the following research results. (1) New methods for temporal property verification of higher-order programs. (2) New results on cyclic proof systems,formal deduction systems for mathematical induction, and new methods for deciding validity of formulas in first-order fixpoint logic with background theories. (3) A new type and effect system for verifying temporal properties of programs with algebraic effects and handlers, an emerging programming language feature for uniformly expressing a variety of computational effects including destructive updates. (4) Research achievements on the application of program verification and synthesis techniques to security, such as a method for repairing real-world regular expressions vulnerable to ReDoS attacks. (5) New results on the formal language theory of regular expressions extended with real-world features such as backreferences and lookaheads.

  12. Program Verification Based on Higher-Order Fixpoint Logic

    Offer Organization: Japan Society for the Promotion of Science

    System: Grants-in-Aid for Scientific Research

    Category: Grant-in-Aid for Scientific Research (A)

    Institution: The University of Tokyo

    2020/04/01 - 2021/03/31

  13. Theory of Gradual Typing for Modern Programming Languages Competitive

    Atsushi Igarashi

    Offer Organization: Japan Society for the Promotion of Science

    System: Grant-in-Aid for Scientific Research (B)

    Category: Grant-in-Aid for Scientific Research (B)

    Institution: Kyoto University

    2017/04 - 2021/03

    More details Close

    Gradual typing is a programming-language technique that allows statically typed and dynamically typed parts to coexist in a single program. We have studied the theoretical foundations for applying this technique to advanced programming languages. The main result is computational calculi that introduce gradual typing to advanced programming language mechanisms such as polymorphism, session types, refinement types, nondeterminism, ML type inference, and intersection types; we have proved its properties (such as type safety). In addition, we improved space-efficient coercions that have been proposed as an implementation technique for gradual typing by coercion passing style compilation, which we implemented and evaluated.

  14. Temporal and Relational Verification of High-Level Programs Competitive

    Hiroshi Unno

    Offer Organization: Japan Society for the Promotion of Science

    System: Grant-in-Aid for Young Scientists (A)

    Category: Grant-in-Aid for Young Scientists (A)

    Institution: University of Tsukuba

    2016/04 - 2020/03

    More details Close

    In this research, we have extended verification methods and tools based on refinement types and constrained Horn clauses to enable relational and temporal verification of high-level programs. For relational verification, we have proposed Horn constraint solving methods based on (co-)inductive theorem proving. We have also presented methods for solving first-order fixpoint logic constraints to enable temporal verification.

  15. Refinement and Extension of Higher-Order Model Checking Competitive

    Naoki Kobayashi

    Offer Organization: Japan Society for the Promotion of Science

    System: Grant-in-Aid for Scientific Research (S)

    Category: Grant-in-Aid for Scientific Research (S)

    Institution: The University of Tokyo

    2015/04 - 2020/03

    More details Close

    This research aimed to advance the theory of higher-order model checking and its applications. We have obtained good theoretical results, such as a pumping lemma for higher-order languages and the surprising connection between two kinds of higher-order model checking. We have also made progress in the applications of higher-order model checking, such as the big improvement in the efficiency of higher-order model checkers and program verification tools and in the class of program properties that can be verified, and a new technique for higher-order data compression using arithmetic coding.

  16. Study on Highly Reliable Programming Languages for Code Generation Competitive

    Yukiyoshi Kameyama

    Offer Organization: Japan Society for the Promotion of Science

    System: Grant-in-Aid for Scientific Research (B)

    Category: Grant-in-Aid for Scientific Research (B)

    Institution: University of Tsukuba

    2013/04 - 2016/03

    More details Close

    Code generation is a leading approach to generate, for a given generic program, specialized code for individual environments, parameters, and architectures. In this research we have developed theories and programming languages for safe and highly reliable code generation, and have also implemented them. Our major results include: (1) We succeeded in designing and implementing a new type system in which one can use various side effects such as mutation and control operators as well as can write code generators, yet the system ensures well typedness and well scopedness statically. (2) We have designed and implemented a new language for generating efficient database queries in SQL that is type safe. (3) We have proposed an automatic technique for inserting staging annotations to programs that are guaranteed to be optimal. We believe that these results and many others of our research contributed to enhance the safety and reliability of program generation techniques.

  17. Extensions and Applications of Refinement Types based on Game Semantics Competitive

    Hiroshi Unno

    Offer Organization: Japan Society for the Promotion of Science

    System: Grant-in-Aid for Young Scientists (B)

    Category: Grant-in-Aid for Young Scientists (B)

    Institution: University of Tsukuba

    2013/04 - 2016/03

    More details Close

    The aim of this research project was to extend refinement type systems and their type checking and inference methods based on a denotational semantics, with applications to formal verification of high-level programs. The main result is the development of a fully-automated tool RCaml for path-sensitive verification of (a) termination, (b) non-termination, and (c) relational properties of high-order functional programs that manipulate algebraic data structures.

  18. Higher-Order Model Checking and its Applications Competitive

    Naoki Kobayashi

    Offer Organization: Japan Society for the Promotion of Science

    System: Grant-in-Aid for Scientific Research (S)

    Category: Grant-in-Aid for Scientific Research (S)

    2011/04 - 2016/03

    More details Close

    The main topic of this research project was higher-order model checking, which is an extension of model checking, a representative method for system verification. In 2009, Kobayashi, the leader of this project, has developed the first practical algorithm for higher-order model checking, and also shown that higher-order model checking is useful for program verification. This research project has been launched to extend his results. The major results include: the development of much faster higher-order model checkers, implementation of fully-automated tools for program verification, and applications to data compression (where data are compressed in the form of functional programs that generate them, and compressed data are manipulated without decompression).

Show all Show first 5