7 citations · 11 across the 7 of their papers we have counts for
9 papers
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…
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…
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…
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…