2 citations · 2 across the 4 of their papers we have counts for
5 papers
Law and Order for Typestate with Borrowing
Hannes Saffrich, Yuki Nishida, Peter Thiemann
Typestate systems are notoriously complex as they require sophisticated machinery for tracking aliasing. We propose a new, transition-oriented foundation for typestate in the setti…
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…