53 citations · 145 across the 24 of their papers we have counts for
7 papers · 1 filter
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…
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;…
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…
Resource Usage Analysis for the Pi-Calculus
Naoki Kobayashi, Kohei Suenaga, Lucian Wischik
We propose a type-based resource usage analysis for the π-calculus extended with resource creation/access primitives. The goal of the resource usage analysis is to statically…