53 citations · 145 across the 24 of their papers we have counts for
25 papers
StatWhy: Formal Verification Tool for Statistical Hypothesis Testing Programs
Yusuke Kawamoto, Kentaro Kobayashi, Kohei Suenaga
Statistical methods have been widely misused and misinterpreted in various scientific fields, raising significant concerns about the integrity of scientific research. To mitigate t…
Probabilistic Black-Box Checking via Active MDP Learning
Junya Shijubo, Masaki Waga, Kohei Suenaga
We introduce a novel methodology for testing stochastic black-box systems, frequently encountered in embedded systems. Our approach enhances the established black-box checking (BBC…
Learning nonlinear hybrid automata from input--output time-series data
Amit Gurung, Masaki Waga, Kohei Suenaga
Learning an automaton that approximates the behavior of a black-box system is a long-studied problem. Besides its theoretical significance, its application to search-based testing…
BOREx: Bayesian-Optimization--Based Refinement of Saliency Map for Image- and Video-Classification Models
Atsushi Kikuchi, Kotaro Uchida, Masaki Waga +1
Explaining a classification result produced by an image- and video-classification model is one of the important but challenging issues in computer vision. Many methods have been pr…
Formalizing Statistical Causality via Modal Logic
Yusuke Kawamoto, Tetsuya Sato, Kohei Suenaga
We propose a formal language for describing and explaining statistical causality. Concretely, we define Statistical Causality Language (StaCL) for expressing causal effects and spe…
Sound and Relatively Complete Belief Hoare Logic for Statistical Hypothesis Testing Programs
Yusuke Kawamoto, Tetsuya Sato, Kohei Suenaga
We propose a new approach to formally describing the requirement for statistical inference and checking whether a program uses the statistical method appropriately. Specifically, w…
Goal-Aware RSS for Complex Scenarios via Program Logic
Ichiro Hasuo, Clovis Eberhart, James Haydon +12
We introduce a goal-aware extension of responsibility-sensitive safety (RSS), a recent methodology for rule-based safety guarantee for automated driving systems (ADS). Making RSS r…
Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption
Ryotaro Banno, Kotaro Matsuoka, Naoki Matsumoto +3
In many Internet of Things (IoT) applications, data sensed by an IoT device are continuously sent to the server and monitored against a specification. Since the data often contain…
The Lattice-Theoretic Essence of Property Directed Reachability Analysis
Mayuko Kori, Natsuki Urabe, Shin-ya Katsumata +2
We present LT-PDR, a lattice-theoretic generalization of Bradley's property directed reachability analysis (PDR) algorithm. LT-PDR identifies the essence of PDR to be an ingenious…
Efficient Black-Box Checking via Model Checking with Strengthened Specifications
Junya Shijubo, Masaki Waga, Kohei Suenaga
Black-box checking (BBC)} is a testing method for cyber-physical systems (CPSs) as well as software systems. BBC consists of active automata learning and model checking; a Mealy ma…
HELMHOLTZ: A Verifier for Tezos Smart Contracts Based on Refinement Types
Yuki Nishida, Hiromasa Saito, Ran Chen +4
A smart contract is a program executed on a blockchain, based on which many cryptocurrencies are implemented, and is being used for automating transactions. Due to the large amount…
Learning Heuristics for Template-based CEGIS of Loop Invariants with Reinforcement Learning
Minchao Wu, Takeshi Tsukada, Hiroshi Unno +2
Loop-invariant synthesis is the basis of program verification. Due to the undecidability of the problem in general, a tool for invariant synthesis necessarily uses heuristics. Desp…
Verification of a Merkle Patricia Tree Library Using F*
Sota Sato, Ryotaro Banno, Jun Furuse +2
A Merkle tree is a data structure for representing a key-value store as a tree. Each node of a Merkle tree is equipped with a hash value computed from those of their descendants. A…
Control-Data Separation and Logical Condition Propagation for Efficient Inference on Probabilistic Programs
Ichiro Hasuo, Yuichiro Oyabu, Clovis Eberhart +3
We present a novel sampling framework for probabilistic programs. The framework combines two recent ideas -- \emph{control-data separation} and \emph{logical condition propagation}…
Visualizing Color-wise Saliency of Black-Box Image Classification Models
Yuhki Hatakeyama, Hiroki Sakuma, Yoshinori Konishi +1
Image classification based on machine learning is being commonly used. However, a classification result given by an advanced method, including deep learning, is often hard to inter…
ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs
John Toman, Ren Siqi, Kohei Suenaga +2
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…
Generalized Property-Directed Reachability for Hybrid Systems
Kohei Suenaga, Takuya Ishizawa
Generalized property-directed reachability (GPDR) belongs to the family of the model-checking techniques called IC3/PDR. It has been successfully applied to software verification;…
MONAA: A Tool for Timed Pattern Matching with Automata-Based Acceleration
Masaki Waga, Ichiro Hasuo, Kohei Suenaga
We present monaa, a monitoring tool over a real-time property specified by either a timed automaton or a timed regular expression. It implements a timed pattern matching algorithm…
Automated proof synthesis for propositional logic with deep neural networks
Taro Sekiyama, Kohei Suenaga
This work explores the application of deep learning, a machine learning technique that uses deep neural networks (DNN) in its core, to an automated theorem proving (ATP) problem. T…
Sharper and Simpler Nonlinear Interpolants for Program Verification
Takamasa Okudono, Yuki Nishida, Kensuke Kojima +3
Interpolation of jointly infeasible predicates plays important roles in various program verification techniques such as invariant synthesis and CEGAR. Intrigued by the recent resul…
Efficient Online Timed Pattern Matching by Automata-Based Skipping
Masaki Waga, Ichiro Hasuo, Kohei Suenaga
The timed pattern matching problem is an actively studied topic because of its relevance in monitoring of real-time systems. There one is given a log and a specification $\math…
Towards Proof Synthesis Guided by Neural Machine Translation for Intuitionistic Propositional Logic
Taro Sekiyama, Akifumi Imanishi, Kohei Suenaga
Inspired by the recent evolution of deep neural networks (DNNs) in machine learning, we explore their application to PL-related topics. This paper is the first step towards this go…
Generalized Homogeneous Polynomials for Efficient Template-Based Nonlinear Invariant Synthesis
Kensuke Kojima, Minoru Kinoshita, Kohei Suenaga
The template-based method is one of the most successful approaches to algebraic invariant synthesis. In this method, an algorithm designates a template polynomial p over program va…
Input Synthesis for Sampled Data Systems by Program Logic
Takumi Akazaki, Ichiro Hasuo, Kohei Suenaga
Inspired by a concrete industry problem we consider the input synthesis problem for hybrid systems: given a hybrid system that is subject to input from outside (also called disturb…