Search

The decidability of the reachability problem for finitary PCF has been used as a theoretical basis for fully automated verification tools for functional programs. The reachability problem, however, often becomes undecidable for a slight extension of finitary PCF with side effects, such as exceptions, algebraic effects, and references, which hindered the extension of the above verification tools for supporting functional programs with side effects. In this paper, we first give simple proofs of the undecidability of four extensions of finitary PCF, which would help us understand and analyze the source of undecidability. We then focus on an extension with references, and give a decidable fragment using a type system. To our knowledge, this is the first non-trivial decidable fragment that features higher-order recursive functions containing reference cells.

Toman et al. have proposed a type system for automatic verification of low-level programs, which combines ownership types and refinement types to enable strong updates of refinement types in the presence of pointer aliases. We extend their type system to support pointer arithmetic, and prove its soundness. Based on the proposed type system, we have implemented a prototype tool for automated verification of the lack of assertion errors of low-level programs with pointer arithmetic, and confirmed its effectiveness through experiments., Comment: An extended version of the paper to appear in Proceedings of PEPM 2024

Automated verification of functional correctness of imperative programs with references (a.k.a. pointers) is challenging because of reference aliasing. Ownership types have recently been applied to address this issue, but the existing approaches were limited in that they are effective only for a class of programs whose reference usage follows a certain style. To relax the limitation, we combine the approaches of ConSORT (based on fractional ownership) and RustHorn (based on borrowable ownership), two recent approaches to automated program verification based on ownership types, and propose the notion of borrowable fractional ownership types. We formalize a new type system based on the borrowable fractional ownership types and show how we can use it to automatically reduce the program verification problem for imperative programs with references to that for functional programs without references. We also show the soundness of our type system and the translation, and conduct experiments to confirm the effectiveness of our approach., Comment: An extended version of the paper to appear in Proceedings of VMCAI 2024

To promote and further develop RST-style discourse parsing models, we need a strong baseline that can be regarded as a reference for reporting reliable experimental results. This paper explores a strong baseline by integrating existing simple parsing strategies, top-down and bottom-up, with various transformer-based pre-trained language models. The experimental results obtained from two benchmark datasets demonstrate that the parsing performance strongly relies on the pretrained language models rather than the parsing strategies. In particular, the bottom-up parser achieves large performance gains compared to the current best parser when employing DeBERTa. We further reveal that language models with a span-masking scheme especially boost the parsing performance through our analysis within intra- and multi-sentential parsing, and nuclearity prediction., Comment: Accepted in Findings of EMNLP 2022

We consider the reachability problem for higher-order functional programs and study the relationship between reachability games (i.e., the reachability problem for programs with angelic and demonic nondeterminism) and may-reachability (i.e., the reachability problem for programs with only angelic nondeterminism). We show that reachability games for order-n programs can be reduced to may-reachability for order-(n+1) programs, and vice versa. We formalize the reductions by using higher-order fixpoint logic and prove their correctness. We also discuss applications of the reductions to higher-order program verification.

Tensor shape mismatch is a common source of bugs in deep learning programs. We propose a new type-based approach to detect tensor shape mismatches. One of the main features of our approach is the best-effort shape inference. As the tensor shape inference problem is undecidable in general, we allow static type/shape inference to be performed only in a best-effort manner. If the static inference cannot guarantee the absence of the shape inconsistencies, dynamic checks are inserted into the program. Another main feature is gradual typing, where users can improve the precision of the inference by adding appropriate type annotations to the program. We formalize our approach and prove that it satisfies the criteria of gradual typing proposed by Siek et al. in 2015. We have implemented a prototype shape checking tool based on our approach and evaluated its effectiveness by applying it to some deep neural network programs., Comment: 48 pages

We propose an automated method for checking the validity of a formula of HFL(Z), a higher-order logic with fixpoint operators and integers. Combined with Kobayashi et al.'s reduction from higher-order program verification to HFL(Z) validity checking, our method yields a fully automated, uniform verification method for arbitrary temporal properties of higher-order functional programs expressible in the modal mu-calculus, including termination, non-termination, fair termination, fair non-termination, and also branching-time properties. We have implemented our method and obtained promising experimental results., Comment: A long version of the paper published in Proceedings of POPL 2023

The fragment-size distributions of raw carrot diced or crushed using a food mixer are studied experimentally. For the 5-mm-square raw carrot, the normal distribution shows a characteristic feature of food fragmentation statistics. This simple result indicates that most random errors contribute to fragment-size fluctuation. On the other hand, for the crushed raw carrot, the cumulative fragment size distribution follows the power law where the exponent $\alpha \simeq 1.62 > 1$. Furthermore, considering the cumulative fragment-size distribution as a function of length for comparison with geomaterials, such as fault rocks, the exponent $D \simeq 3.64$. Previous studies have shown that the power-law distribution observed in sequential fragmentation tends to have a large exponent value. As our experiment is also based on sequential fragmentation, the obtained large values of exponents $\alpha$ and $D$ are consistent with those obtained in previous studies on sequential fragmentation. On the basis of previous studies and our observations, we discuss the effect of the preferential fragmentation of particles as large as the mixer blades. We also discuss the existence of a lower limit beyond which further fragmentation is difficult, resulting in a power-law distribution tendency for raw carrot crushed with a food mixer., Comment: 5 pages, 5 figures

In this article, we give an overview of our project on higher-order program verification based on HFL (higher-order fixpoint logic) model checking. After a brief introduction to HFL, we explain how it can be applied to program verification, and summarize the current status of the project., Comment: In Proceedings HCVS 2021, arXiv:2109.03988

We propose an automated method for proving termination of $\pi$-calculus processes, based on a reduction to termination of sequential programs: we translate a $\pi$-calculus process to a sequential program, so that the termination of the latter implies that of the former. We can then use an off-the-shelf termination verification tool to check termination of the sequential program. Our approach has been partially inspired by Deng and Sangiorgi's termination analysis for the $\pi$-calculus, and checks that there is no infinite chain of communications on replicated input channels, by converting such a chain of communications to a chain of recursive function calls in the target sequential program. We have implemented an automated tool based on the proposed method and confirmed its effectiveness., Comment: A shorter version will appear in Proceedings of APLAS 2021

Despite the recent advance of automated program verification, reasoning about recursive data structures remains as a challenge for verification tools and their backends such as SMT and CHC solvers. To address the challenge, we introduce the notion of symbolic automatic relations (SARs), which combines symbolic automata and automatic relations, and inherits their good properties such as the closure under Boolean operations. We consider the satisfiability problem for SARs, and show that it is undecidable in general, but that we can construct a sound (but incomplete) and automated satisfiability checker by a reduction to CHC solving. We discuss applications to SMT and CHC solving on data structures, and show the effectiveness of our approach through experiments., Comment: A shorter version will appear in Proceedings of SAS 2021

We address the problem of analysing the complexity of concurrent programs written in Pi-calculus. We are interested in parallel complexity, or span, understood as the execution time in a model with maximal parallelism. A type system for parallel complexity has been recently proposed by Baillot and Ghyselen but it is too imprecise for non-linear channels and cannot analyse some concurrent processes. Aiming for a more precise analysis, we design a type system which builds on the concepts of sized types and usages. The new variant of usages we define accounts for the various ways a channel is employed and relies on time annotations to track under which conditions processes can synchronize. We prove that a type derivation for a process provides an upper bound on its parallel complexity.

We propose a novel framework of program and invariant synthesis called neural network-guided synthesis. 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., Comment: A summary will appear in Proceedings of SAS 2021, Springer LNCS

We introduce PHFL, a probabilistic extension of higher-order fixpoint logic, which can also be regarded as a higher-order extension of probabilistic temporal logics such as PCTL and the $\mu^p$-calculus. We show that PHFL is strictly more expressive than the $\mu^p$-calculus, and that the PHFL model-checking problem for finite Markov chains is undecidable even for the $\mu$-only, order-1 fragment of PHFL. Furthermore the full PHFL is far more expressive: we give a translation from Lubarsky's $\mu$-arithmetic to PHFL, which implies that PHFL model checking is $\Pi^1_1$-hard and $\Sigma^1_1$-hard. As a positive result, we characterize a decidable fragment of the PHFL model-checking problems using a novel type system.

A cyclic proof system allows us to perform inductive reasoning without explicit inductions. We propose a cyclic proof system for HFLN, which is a higher-order predicate logic with natural numbers and alternating fixed-points. Ours is the first cyclic proof system for a higher-order logic, to our knowledge. Due to the presence of higher-order predicates and alternating fixed-points, our cyclic proof system requires a more delicate global condition on cyclic proofs than the original system of Brotherston and Simpson. We prove the decidability of checking the global condition and soundness of this system, and also prove a restricted form of standard completeness for an infinitary variant of our cyclic proof system. A potential application of our cyclic proof system is semi-automated verification of higher-order programs, based on Kobayashi et al.'s recent work on reductions from program verification to HFLN validity checking., Comment: 27 pages

We propose a new approach for universal lossless text compression, based on grammar compression. In the literature, a target string $T$ has been compressed as a context-free grammar $G$ in Chomsky normal form satisfying $L(G) = \{T\}$. Such a grammar is often called a \emph{straight-line program} (SLP). In this paper, we consider a probabilistic grammar $G$ that generates $T$, but not necessarily as a unique element of $L(G)$. In order to recover the original text $T$ unambiguously, we keep both the grammar $G$ and the derivation tree of $T$ from the start symbol in $G$, in compressed form. We show some simple evidence that our proposal is indeed more efficient than SLPs for certain texts, both from theoretical and practical points of view., Comment: 11 pages, 3 figures, accepted for poster presentation at DCC 2020

Reduction to the satisfiability problem for constrained Horn clauses (CHCs) is a widely studied approach to automated program verification. The current CHC-based methods for pointer-manipulating programs, however, are not very scalable. This paper proposes a novel translation of pointer-manipulating Rust programs into CHCs, which clears away pointers and memories by leveraging ownership. We formalize the translation for a simplified core of Rust and prove its correctness. We have implemented a prototype verifier for a subset of Rust and confirmed the effectiveness of our method., Comment: Full version of the same-titled paper in ESOP2020

We present ConSORT, a type system for safety verification in the presence of mutability and aliasing. Mutability requires strong updates to model changing invariants during program execution, but aliasing between pointers makes it difficult to determine which invariants must be updated in response to mutation. Our type system addresses this difficulty with a novel combination of refinement types and fractional ownership types. Fractional ownership types provide flow-sensitive and precise aliasing information for reference variables. ConSORT interprets this ownership information to soundly handle strong updates of potentially aliased references. We have proved ConSORT sound and implemented a prototype, fully automated inference tool. We evaluated our tool and found it verifies non-trivial programs including data structure implementations.

Higher-order modal fixpoint logic (HFL) is a higher-order extension of the modal mu-calculus, and strictly more expressive than the modal mu-calculus. It has recently been shown that various program verification problems can naturally be reduced to HFL model checking: the problem of whether a given finite state system satisfies a given HFL formula. In this paper, we propose a novel algorithm for HFL model checking: it is the first practical algorithm in that it runs fast for typical inputs, despite the hyper-exponential worst-case complexity of the HFL model checking problem. Our algorithm is based on Kobayashi et al.'s type-based characterization of HFL model checking, and was inspired by a saturation-based algorithm for HORS model checking, another higher-order extension of model checking. We prove the correctness of the algorithm and report on an implementation and experimental results., Comment: A longer version of APLAS 2019 paper

In the last two decades, there has been much progress on model checking of both probabilistic systems and higher-order programs. In spite of the emergence of higher-order probabilistic programming languages, not much has been done to combine those two approaches. In this paper, we initiate a study on the probabilistic higher-order model checking problem, by giving some first theoretical and experimental results. As a first step towards our goal, we introduce PHORS, a probabilistic extension of higher-order recursion schemes (HORS), as a model of probabilistic higher-order programs. The model of PHORS may alternatively be viewed as a higher-order extension of recursive Markov chains. We then investigate the probabilistic termination problem -- or, equivalently, the probabilistic reachability problem. We prove that almost sure termination of order-2 PHORS is undecidable. We also provide a fixpoint characterization of the termination probability of PHORS, and develop a sound (but possibly incomplete) procedure for approximately computing the termination probability. We have implemented the procedure for order-2 PHORSs, and confirmed that the procedure works well through preliminary experiments that are reported at the end of the article.

A capturing system with multispectral filter array (MSFA) technology is proposed for shortening the capture time and reducing costs. Therein, a mosaicked image captured using an MSFA is demosaicked to reconstruct multispectral images (MSIs). Joint optimization of the spectral sensitivity of the MSFAs and demosaicking is considered, and pathology-specific multispectral imaging is proposed. This optimizes the MSFA and the demosaicking matrix by minimizing the reconstruction error between the training data of a hematoxylin and eosin-stained pathological tissue and a demosaicked MSI using a cost function. Initially, the spectral sensitivity of the filter array is set randomly and the mosaicked image is obtained from the training data. Subsequently, a reconstructed image is obtained using Wiener estimation. To minimize the reconstruction error, the spectral sensitivity of the filter array and the Wiener estimation matrix are optimized iteratively through an interior-point approach. The effectiveness of the proposed MSFA and demosaicking is demonstrated by comparing the recovered spectrum and RGB image with those obtained using a conventional method.

A capturing system with multispectral filter array (MSFA) technology has been researched to shorten the capturing time and reduce the cost. In this system, the mosaicked image captured by the MSFA is demosaicked to reconstruct multispectral images (MSIs). We focus on the spectral sensitivity design of a MSFA in this paper and propose a pathology-specific MSFA. The proposed method optimizes the MSFA by minimizing the reconstruction error between training data of a pathological tissue and a demosaicked MSI under a cost function. Firstly, the spectral sensitivities of the filter array are set randomly, and the mosaicked image is obtained from the training data and the filter array. Then, a reconstructed image is obtained by Wiener estimation. The spectral sensitivities of the filter array are optimized iteratively by an interior-point approach to minimize the reconstruction error. We show the effectiveness of the proposed MSFA by comparing the recovered spectrum and RGB image with a conventional method.