4 papers
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…
Compilation of Coordinated Choice
Yuki Nishida, Atsushi Igarashi
Recently, we have proposed coordinated choices, which are nondeterministic choices equipped with names. The main characteristic of coordinated choices is that they synchronize nond…
Manifest Contracts with Intersection Types
Yuki Nishida, Atsushi Igarashi
We present a manifest contract system PCFvH with intersection types. A manifest contract system is a typed functional calculus in which software contracts are integrated into a…
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…