研究者詳細

顔写真

ウンノ　ヒロシ
海野　広志
Hiroshi Unno
所属
電気通信研究所　計算システム基盤研究部門　ソフトウエア構成研究室
職名
教授
学位

  • 博士（情報理工学） （東京大学）

e-Rad 研究者番号
80569575

所属学協会 2

  • 日本ソフトウェア科学会

  • ACM

研究キーワード 5

  • 定理自動証明

  • モデル検査

  • 型システム

  • 形式検証

  • プログラミング言語

研究分野 2

  • 情報通信 / ソフトウェア /

  • 情報通信 / 情報学基礎論 /

論文 48

  1. A Hierarchy of Supermartingales for ω-Regular Verification 査読有り

    Satoshi Kura, Hiroshi Unno

    Proceedings of the ACM on Programming Languages　2026年6月8日

    DOI： 10.1145/3808257 　

  2. Supermartingales for Unique Fixed Points: A Unified Approach to Lower Bound Verification 査読有り

    Satoshi Kura, Hiroshi Unno, Takeshi Tsukada

    Proceedings of the ACM on Programming Languages　2026年6月8日

    DOI： 10.1145/3808348 　

  3. A Category-Theoretic Framework for Dependent Effect Systems 査読有り

    Satoshi Kura, Marco Gaboardi, Taro Sekiyama, Hiroshi Unno

    Lecture Notes in Computer Science　401-431　2026年4月10日

    出版者・発行元： 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 査読有り

    Taro Sekiyama, Ugo Dal Lago, Hiroshi Unno

    Proceedings of the ACM on Programming Languages　9　(OOPSLA2)　3726-3754　2025年10月9日

    DOI： 10.1145/3763184 　

    eISSN：2475-1421

  5. Thrust: A Prophecy-Based Refinement Type System for Rust 査読有り

    Hiromi Ogawa, Taro Sekiyama, Hiroshi Unno

    Proceedings of the ACM on Programming Languages　9　(PLDI)　2056-2080　2025年6月10日

    出版者・発行元： Association for Computing Machinery (ACM)

    DOI： 10.1145/3729333 　

    eISSN：2475-1421

    詳細を見る 詳細を閉じる

    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 査読有り

    Hiroshi Unno, Takeshi Tsukada, Jie-Hong Roland Jiang

    Proceedings of the AAAI Conference on Artificial Intelligence　39　(11)　11372-11380　2025年4月11日

    出版者・発行元： Association for the Advancement of Artificial Intelligence (AAAI)

    DOI： 10.1609/aaai.v39i11.33237 　

    ISSN：2159-5399

    eISSN：2374-3468

    詳細を見る 詳細を閉じる

    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 招待有り 査読有り

    Naoki Kobayashi, Taro Sekiyama, Issei Sato, Hiroshi Unno

    Formal Methods in System Design　2025年2月24日

    出版者・発行元： Springer Science and Business Media LLC

    DOI： 10.1007/s10703-024-00468-9 　

    ISSN：0925-9856

    eISSN：1572-8102

    詳細を見る 詳細を閉じる

    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 査読有り

    Taro Sekiyama, Hiroshi Unno

    Proceedings of the ACM on Programming Languages　9　(POPL)　2306-2336　2025年1月7日

    出版者・発行元： Association for Computing Machinery (ACM)

    DOI： 10.1145/3704914 　

    eISSN：2475-1421

    詳細を見る 詳細を閉じる

    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 査読有り

    Takeshi Tsukada, Hiroshi Unno, Oded Padon, Sharon Shoham

    Proceedings of the ACM on Programming Languages　9　(POPL)　2025-2056　2025年1月7日

    出版者・発行元： Association for Computing Machinery (ACM)

    DOI： 10.1145/3704904 　

    eISSN：2475-1421

    詳細を見る 詳細を閉じる

    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 査読有り

    Taro Sekiyama, Hiroshi Unno

    Proceedings of the ACM on Programming Languages　8　(OOPSLA2)　2662-2691　2024年10月8日

    出版者・発行元： Association for Computing Machinery (ACM)

    DOI： 10.1145/3689805 　

    eISSN：2475-1421

    詳細を見る 詳細を閉じる

    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 査読有り

    Satoshi Kura, Hiroshi Unno

    Proceedings of the ACM on Programming Languages　8　(ICFP)　973-1002　2024年8月15日

    出版者・発行元： Association for Computing Machinery (ACM)

    DOI： 10.1145/3674662 　

    eISSN：2475-1421

    詳細を見る 詳細を閉じる

    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 査読有り

    Takeshi Tsukada, Hiroshi Unno

    Proceedings of the ACM on Programming Languages　8　(PLDI)　1979-2002　2024年6月20日

    出版者・発行元： Association for Computing Machinery (ACM)

    DOI： 10.1145/3656457 　

    eISSN：2475-1421

    詳細を見る 詳細を閉じる

    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 査読有り

    Fuga Kawamata, Hiroshi Unno, Taro Sekiyama, Tachio Terauchi

    Proceedings of the ACM on Programming Languages　8　(POPL)　115-147　2024年1月5日

    出版者・発行元： Association for Computing Machinery (ACM)

    DOI： 10.1145/3633280 　

    eISSN：2475-1421

    詳細を見る 詳細を閉じる

    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 査読有り

    Hiroshi Unno, Tachio Terauchi, Yu Gu, Eric Koskinen

    Proceedings of the ACM on Programming Languages　7　(POPL)　2111-2140　2023年1月9日

    出版者・発行元： Association for Computing Machinery (ACM)

    DOI： 10.1145/3571265 　

    eISSN：2475-1421

    詳細を見る 詳細を閉じる

    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. 査読有り

    Yu Gu, Takeshi Tsukada, Hiroshi Unno 0001

    Proc. ACM Program. Lang.　7　(POPL)　604-631　2023年1月

    DOI： 10.1145/3571214 　

  16. 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　(POPL)　2079-2110　2023年1月

    DOI： 10.1145/3571264 　

  17. Software model-checking as cyclic-proof search 査読有り

    Takeshi Tsukada, Hiroshi Unno

    Proceedings of the ACM on Programming Languages　6　(POPL)　1-29　2022年1月16日

    出版者・発行元： Association for Computing Machinery (ACM)

    DOI： 10.1145/3498725 　

    eISSN：2475-1421

    詳細を見る 詳細を閉じる

    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. 査読有り

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

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

    出版者・発行元： Springer

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

  19. Constraint-Based Relational Verification 査読有り

    Hiroshi Unno, Tachio Terauchi, Eric Koskinen

    Computer Aided Verification　742-766　2021年

    出版者・発行元： Springer International Publishing

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

    ISSN：0302-9743

    eISSN：1611-3349

    詳細を見る 詳細を閉じる

    <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 査読有り

    Satoshi Kura, Hiroshi Unno, Ichiro Hasuo

    Computer Aided Verification　75-98　2021年

    出版者・発行元： Springer International Publishing

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

    ISSN：0302-9743

    eISSN：1611-3349

    詳細を見る 詳細を閉じる

    <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年4月3日

    出版者・発行元： Association for the Advancement of Artificial Intelligence (AAAI)

    DOI： 10.1609/aaai.v34i02.5526 　

    ISSN：2159-5399

    eISSN：2374-3468

    詳細を見る 詳細を閉じる

    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 招待有り 査読有り

    KIMURA Daisuke, NAKAZAWA Koji, TERAUCHI Tachio, UNNO Hiroshi

    コンピュータ ソフトウェア　37　(1)　1_39-1_52　2020年

    出版者・発行元： 日本ソフトウェア科学会

    DOI： 10.11309/jssst.37.1_39 　

    ISSN：0289-6540

    詳細を見る 詳細を閉じる

    <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 査読有り

    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 査読有り

    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 査読有り

    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 査読有り

    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 査読有り

    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年

    出版者・発行元： Springer Verlag

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

    ISSN：1611-3349 0302-9743

  28. Temporal verification of higher-order functional programs 査読有り

    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 査読有り

    Hiroshi Unno, Naoshi Tabuchi, Naoki Kobayashi

    MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE　25　(4)　841-866　2015年5月

    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年

    出版者・発行元： Japan Society for Software Science and Technology

    ISSN：0289-6540

  31. Relaxed Stratification: A New Approach to Practical Complete Predicate Refinement 査読有り

    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 査読有り

    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年

    出版者・発行元： Springer Verlag

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

    ISSN：1611-3349 0302-9743

  33. Refinement Type Inference via Horn Constraint Optimization 査読有り

    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 査読有り

    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年

    出版者・発行元： 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 査読有り

    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 査読有り

    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 査読有り

    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 査読有り

    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 査読有り

    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 査読有り

    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 査読有り

    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 査読有り

    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 査読有り

    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 査読有り

    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 査読有り

    Hiroshi Unno, Tachio Terauchi, Naoki Kobayashi

    ACM SIGPLAN NOTICES　48　(1)　75-86　2013年1月

    DOI： 10.1145/2480359.2429081 　

    ISSN：0362-1340

︎全件表示 ︎最初の5件までを表示

講演・口頭発表等 8

  1. Fixpoint Logics and Their Applications to Software Verification 招待有り

    Hiroshi Unno

    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 招待有り

    Hiroshi Unno

    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 招待有り

    Hiroshi Unno

    “CHoCoLa” meetings Curry-Howard: Logic and Computation　2025年5月15日

  4. Automating Relational Verification of Infinite-State Programs 招待有り

    Hiroshi Unno

    25th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2024)　2024年1月16日

  5. Constraint-based Relational Verification 招待有り

    Hiroshi Unno

    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日

︎全件表示 ︎最初の5件までを表示

共同研究・競争的資金等の研究課題 18

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

    海野 広志

    2025年4月1日 ～ 2030年3月31日

  2. 並行・並列プログラミングのためのスケーラブルな自動プログラム検証技術

    関山 太朗, 海野 広志

    提供機関：Japan Society for the Promotion of Science

    制度名：Grants-in-Aid for Scientific Research

    研究種目：Grant-in-Aid for Scientific Research (A)

    研究機関：National Institute of Informatics

    2024年4月 ～ 2028年3月

  3. 依存篩型と述語制約によるプログラム検証の深化

    寺内 多智弘, 海野 広志

    提供機関：Japan Society for the Promotion of Science

    制度名：Grants-in-Aid for Scientific Research

    研究種目：Grant-in-Aid for Scientific Research (B)

    研究機関：Waseda University

    2024年4月1日 ～ 2027年3月31日

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

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

    2024年4月1日 ～ 2027年3月31日

  5. 依存篩型と述語制約によるプログラム検証の深化

    寺内 多智弘, 海野 広志

    提供機関：Japan Society for the Promotion of Science

    制度名：Grants-in-Aid for Scientific Research

    研究種目：Grant-in-Aid for Scientific Research (B)

    研究機関：Waseda University

    2022年4月1日 ～ 2027年3月31日

    詳細を見る 詳細を閉じる

    無限状態プログラムの時相論理仕様の検証など様々なプログラム検証の問題を表現することのできる一階不動点論理(first-order fixpoint logic)に関する研究を行った。特に、代表者らの先行研究で提案したpfwCSPという述語制約体系に一階不動点論理の妥当性判定を帰着する方法について研究を行った。より具体的には、一階不動点論理が持つ双対性をうまく利用することで、入力論理式とその否定の部分式に対する近似が互いの解空間を削減するために使えることに注目し、入力とその否定を同時並列に効率よく解く新たな妥当性判定の手法を提案した。この研究の成果をまとめた論文はプログラミング言語分野の最高峰の国際会議であるACM Symposium on Principles of Programming Languages(POPL)に採録され、Distingiushed Paper Awardも受賞した。 <BR> 加えて、後方参照(backreference)、先読み(lookahead)、後読み(lookbehind)といった拡張機能を含む拡張正規表現について、正規表現を含むプログラムに対する著名な脆弱性であるReDoS(regular expression denial of service)を修正するプログラム合成手法の研究と、拡張正規表現の形式言語理論に関する研究を行った。前者の研究成果をまとめた論文はセキュリティ分野の最高峰の国際会議であるIEEE Symposium on Security and Privacy (S&P)に採録され、後者の研究成果をまとめた論文は理論計算機科学分野の主要国際会議であるInternational Conference on Formal Structures for Computation and Deduction (FSCD)に採録された。

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

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

    2022年4月1日 ～ 2027年3月31日

    詳細を見る 詳細を閉じる

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

  7. 時相的・関係的仕様からの高レベルプログラム合成

    海野 広志, 南出 靖彦, 寺内 多智弘

    提供機関：Japan Society for the Promotion of Science

    制度名：Grants-in-Aid for Scientific Research

    研究種目：Grant-in-Aid for Scientific Research (B)

    研究機関：Tohoku University

    2024年4月1日 ～ 2025年3月31日

  8. AI時代を見据えたプログラム検証技術

    小林 直樹, 佐藤 亮介, 五十嵐 淳, 塚田 武志, 吉仲 亮, 海野 広志, 関山 太朗, 佐藤 一誠

    提供機関：Japan Society for the Promotion of Science

    制度名：Grants-in-Aid for Scientific Research Grant-in-Aid for Scientific Research (S)

    研究種目：Grant-in-Aid for Scientific Research (S)

    研究機関：The University of Tokyo

    2020年8月31日 ～ 2025年3月31日

    詳細を見る 詳細を閉じる

    研究課題全体を(A)高階モデル検査をはじめとするプログラム検証理論・技術のさらなる発展、(B)プログラム検証への機械学習技術の応用、(C)質の変化したプログラムの検証手法、の3つの課題に分けて並行して研究を進めた。2020年度の主な研究実績（一部、繰越分として2021年度に実施した成果を含む）は以下のとおり。 (A)プログラム検証技術の発展：高階モデル検査の一種である高階不動点論理HFL(Z)の真偽値判定に基づくプログラム検証の統一的枠組みについての研究を進め、HFL(Z)の真偽値判定手法およびその実装を進めた。また、ポインタを扱うプログラムの検証のため、所有権型を持つプログラムの検証問題を、不動点論理の一種であるCHCの充足可能性判定問題に帰着する手法の改良や、"Relational Verification"と呼ばれる、複数のプログラムまたはプログラムの複数の実行間の関係を検証する手法の研究を行い、そられの有効性を確認した。 (B)プログラム検証への機械学習技術の応用：(A)で触れたCHCの充足可能性判定器の改良のため、(i)解の候補のテンプレートの選択に強化学習を応用する方式、(ii)正例・負例データをもとにニューラルネットワークを学習させ、その重み情報を利用して解の候補を発見する方式（NeuGuS: Neural Network Guided Synthesis）を考案し、そられの実装・実験を行って有効性を確認した。 (C)質の変化したプログラムの検証手法： (B)のNeuGuSの枠組みを利用し、一部がオラクルとして未定のプログラムとその仕様を入力とし、オラクル部分の式を自動発見する仕組みを考案し、予備実験を行った。また、確率付きプログラムの検証のための基礎として、確率付き高階不動点論理について研究を行った。

  9. 時相的・関係的仕様からの高レベルプログラム合成

    海野 広志, 南出 靖彦, 寺内 多智弘

    提供機関：Japan Society for the Promotion of Science

    制度名：Grants-in-Aid for Scientific Research Grant-in-Aid for Scientific Research (B)

    研究種目：Grant-in-Aid for Scientific Research (B)

    研究機関：University of Tsukuba

    2020年4月1日 ～ 2025年3月31日

    詳細を見る 詳細を閉じる

    本研究では、ミッションクリティカルシステムの一部としての利用にも耐える高信頼・高効率のプログラムを、必ずしもプログラミングや形式手法の知識を持たないユーザが、少ない労力で得ることが可能な世界の実現を目指し、プログラム検証・合成のための理論構築およびツールの研究・開発を行う。特にオブジェクト指向・関数型言語で記述される高レベルプログラムと時相的・関係的仕様を検証・合成の対象とし、我々が世界をリードする検証理論（リファインメント型・動的論理・不動点論理）・ツールを形式言語理論に基づき発展させることによりプログラム合成も可能とする。本年度は、1階不動点論理の循環証明およびmaximally conservative interpolationに基づくソフトウェアモデル検査の基礎理論構築を行い、その成果をプログラミング言語分野のトップ国際会議であるPOPL 2022で発表した。

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

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

    2019年4月1日 ～ 2024年3月31日

    詳細を見る 詳細を閉じる

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

  11. 高階・再帰的データ構造への破壊的代入を含む高レベル言語プログラムの高精度な検証 競争的資金

    寺内 多智弘

    提供機関：Japan Society for the Promotion of Science

    制度名：Grant-in-Aid for Scientific Research (B)

    研究種目：Grant-in-Aid for Scientific Research (B)

    研究機関：Waseda University

    2017年4月 ～ 2022年3月

    詳細を見る 詳細を閉じる

    再帰データ構造と再帰関数を含むプログラムの時相論理仕様の検証など様々なプログラム検証の問題を表現することのできる一階述語不動点論理(first-order fixpoint logic)に関する研究を行った。特に、constrained Horn clauses(CHCs)を拡張した述語制約クラスの制約解消問題に一階述語不動点論理の定理証明問題を帰着し、制約解消アルゴリズムにより自動定理証明を実現するアルゴリズムを開発した。 <BR> また、前年度に引き続き、再帰データ構造に対する破壊的代入を含むプログラムの検証に適したプログラム論理である分離論理(separation logic)についての研究を行った。特に、分離論理のための循環証明(cyclic proof)探索の自動化についての研究を行った。 <BR> 加えて、タイミング攻撃に対する耐タンパ性の検証に関する研究を行った。この研究ではどのようなプログラムおよび攻撃者に対してbucketingが有効であるのか調査することを目指し、bucketingにより安全性の保証を得るための必要条件および十分条件に関する成果を得た。また、本手法の枠組みで得られる保証の理論的限界についても研究を行った。これらの研究の成果をまとめた論文は国際論文誌Journal of Computer Securityに採録された。

  12. 高階不動点論理に基づくプログラム検証

    小林 直樹, 佐藤 亮介, 五十嵐 淳, 海野 広志

    提供機関：Japan Society for the Promotion of Science

    制度名：Grants-in-Aid for Scientific Research

    研究種目：Grant-in-Aid for Scientific Research (A)

    研究機関：The University of Tokyo

    2020年4月1日 ～ 2021年3月31日

    詳細を見る 詳細を閉じる

    様々な重要な社会基盤がコンピュータによって制御されている今日，ソフトウェアが期待通りの動作をすることを保証するためのプログラム検証技術は今後ますます重要になる．我々はシステム検証技術の主流であるモデル検査の真の拡張である高階モデル検査とそれに基づくプログラム検証手法について世界をリードしてきたが，最近になって高階モデル検査の中でも高階不動点論理に基づく方式が特に有望であることを見出した．そこで本研究では高階不動点論理に基づくプログラム検証の理論をさらに発展させるとともに，他の関連する理論・技術と組み合わせることによって，高階モデル検査に基づくプログラム自動検証手法を実用レベルにまで昇華させることを目指した．採択後数か月で廃止になったため、上記目的の達成には至っていないが、これまでに以下の研究を行った。 まず、最大不動点のみを持つ高階不動点論理に整数を加えて拡張したνHFL(Z)の論理式の真偽値判定手法として、(1) 述語抽象化と高階モデル検査を組み合わせる方式、(2)詳細型システムにおける型推論問題に帰着する方式、の2種類について並行して研究を進め、両者に基づくνHFL(Z)の論理式の自動真偽値判定ツールPaHFLおよびRetHFLを構築した。さらにそれらのツールをプログラムの自動検証に応用し、既存の同目的のツールHorusよりも優れた性能を示すことを確認した。 また、前年度から取り組んでいた高階不動点論理に確率を加えて拡張した確率付き高階不動点論理PHFLの研究を継続し、PHFLモデル検査問題の困難性を解析階層（analytical hierarchy)を用いて特徴づけるとともに、型システムを用いて決定可能な部分クラスを与えた。

  13. 現代的なプログラミング言語のための漸進的型システムの理論 競争的資金

    五十嵐 淳

    提供機関：Japan Society for the Promotion of Science

    制度名：Grant-in-Aid for Scientific Research (B)

    研究種目：Grant-in-Aid for Scientific Research (B)

    研究機関：Kyoto University

    2017年4月 ～ 2021年3月

    詳細を見る 詳細を閉じる

    漸進的型付けはひとつのプログラム中に静的型付けされる部分と動的型付けされる部分を共存させるための、プログラミング言語技術である．これを先進的なプログラミング言語に適用するための理論的基盤の研究を行った．主な成果は、多相性、セッション型、篩型、非決定性、ML型推論、交差型といった先進的なプログラミング言語機構へ漸進的型付けを導入した計算体系を与え、その性質(型安全性など)を証明した．さらに、漸進的型付けの実装技術として提案されている空間効率のよいコアーション計算を改良し、コアーション渡し形式を経由するコンパイル方法を提案し、実際に実装・評価を行い、その効果を確認した．

  14. 高レベル言語で記述されたソフトウェアの時相的・関係的仕様の検証 競争的資金

    海野 広志

    提供機関：Japan Society for the Promotion of Science

    制度名：Grant-in-Aid for Young Scientists (A)

    研究種目：Grant-in-Aid for Young Scientists (A)

    研究機関：University of Tsukuba

    2016年4月 ～ 2020年3月

    詳細を見る 詳細を閉じる

    本研究では、ソフトウェアの信頼性向上を目的とし、これまで研究代表者らが提案してきたリファインメント型システムやホーン節制約解消法といった高レベル言語のための検証理論とそれに基づく全自動検証ツールRCamlを発展させ、高レベルプログラムの関係的・時相的仕様検証を実現した。特に、関係的仕様検証が可能な（余）帰納的定理証明に基づくホーン節制約解消法および時相的仕様検証が可能な不動点論理制約解消法を世界で初めて実現した。

  15. 高階モデル検査の深化と発展 競争的資金

    小林 直樹

    提供機関：Japan Society for the Promotion of Science

    制度名：Grant-in-Aid for Scientific Research (S)

    研究種目：Grant-in-Aid for Scientific Research (S)

    研究機関：The University of Tokyo

    2015年4月 ～ 2020年3月

    詳細を見る 詳細を閉じる

    本研究では、代表者らがこれまで発展させてきた高階モデル検査の理論およびプログラム検証等への応用を発展させることを目的とした。理論面では、高階文法の反復補題についての40年以上ぶりの進展を得るとともに、異なる2種類の高階モデル検査であるHORSモデル検査とHFLモデル検査の間の関係を明らかにするなど、大きな進展が得られた。また応用面でも、高階モデル検査器およびプログラム自動検証器の大幅な高速化、検証できる性質の拡大、高階データ圧縮のための算術符号化などの成果が得られた。

  16. 信頼性の高いコード生成のためのプログラミング言語の実現 競争的資金

    亀山 幸義

    提供機関：Japan Society for the Promotion of Science

    制度名：Grant-in-Aid for Scientific Research (B)

    研究種目：Grant-in-Aid for Scientific Research (B)

    研究機関：University of Tsukuba

    2013年4月 ～ 2016年3月

    詳細を見る 詳細を閉じる

    コード生成法は、特定の環境やパラメータに応じた特化プログラムを生成することにより、プログラムの実行性能を高める手法である。本研究は、コード生成法の安全性と信頼性を高める手法についての理論体系の構築と言語実装を行った。主な成果は、1. さまざまな副作用を許すコード生成言語に対して、生成されるコードが安全であることを保証する型システムの設計および実装に成功した、2.データベース問合せ言語SQLの効率的コードを生成する型安全な体系を設計・実装した、3. 段階的計算の注釈を自動的に最適な位置に挿入する手法を提案した、などである。これらにより、安全で信頼できるコード生成プログラムの構築手法に貢献した。

  17. ゲーム意味論に基づくリファインメント型の拡張とその応用 競争的資金

    海野 広志

    提供機関：Japan Society for the Promotion of Science

    制度名：Grant-in-Aid for Young Scientists (B)

    研究種目：Grant-in-Aid for Young Scientists (B)

    研究機関：University of Tsukuba

    2013年4月 ～ 2016年3月

    詳細を見る 詳細を閉じる

    本研究では、ソフトウェアの信頼性向上のために、高レベルプログラムの形式検証手法の一つであるリファインメント型システムおよびその型検査・推論法の、表示的意味論に基づく拡張を目指した。その主な成果として、代数データ構造を扱う高階関数型プログラムの(a)停止性、(b)非停止性、(c)関係的性質の全自動・高精度検証が可能な検証ツールRCamlの開発が挙げられる。

  18. 高階モデル検査とその応用 競争的資金

    小林 直樹

    提供機関：Japan Society for the Promotion of Science

    制度名：Grant-in-Aid for Scientific Research (S)

    研究種目：Grant-in-Aid for Scientific Research (S)

    2011年4月 ～ 2016年3月

    詳細を見る 詳細を閉じる

    本研究の中心テーマである高階モデル検査とは、代表的なシステム検証手法であるモデル検査の拡張であり、2009年に研究代表者の小林によって初めて現実的な高階モデル検査アルゴリズムおよびプログラム検証への応用が見出された。本研究課題はその結果を受けて行った研究であり、高階モデル検査器の大幅な高速化、高階モデル検査に基づく全自動プログラム検証器の構築、高階モデル検査のデータ圧縮への応用（データをそれを生成する関数型プログラムの形に圧縮し、圧縮したままのデータ操作を実現）などの成果を得た。

︎全件表示 ︎最初の5件までを表示