17 citations · 28 across the 18 of their papers we have counts for
4 papers · 1 filter
Compositional Verification of Smart Contracts Through Communication Abstraction (Extended)
Scott Wesley, Maria Christakis, Jorge A. Navas +3
Solidity smart contracts are programs that manage up to 2^160 users on a blockchain. Verifying a smart contract relative to all users is intractable due to state explosion. Existin…
Logical Characterization of Coherent Uninterpreted Programs
Hari Govind V K, Sharon Shoham, Arie Gurfinkel
An uninterpreted program (UP) is a program whose semantics is defined over the theory of uninterpreted functions. This is a common abstraction used in equivalence checking, compile…
Verifying Verified Code
Siddharth Priya, Xiang Zhou, Yusen Su +3
A recent case study from AWS by Chong et al. proposes an effective methodology for Bounded Model Checking in industry. In this paper, we report on a follow up case study that explo…
Quantifiers on Demand
Arie Gurfinkel, Sharon Shoham, Yakir Vizel
Automated program verification is a difficult problem. It is undecidable even for transition systems over Linear Integer Arithmetic (LIA). Extending the transition system with theo…