1 citations · 1 across the 6 of their papers we have counts for
9 papers
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…
Global Guidance for Local Generalization in Model Checking
Hari Govind V K, YuTing Chen, Sharon Shoham +1
SMT-based model checkers, especially IC3-style ones, are currently the most effective techniques for verification of infinite state systems. They infer global inductive invariants…
Interpolating Strong Induction
Hari Govind V K, Yakir Vizel, Vijay Ganesh +1
The principle of strong induction, also known as k-induction is one of the first techniques for unbounded SAT-based Model Checking (SMC). While elegant and simple to apply, propert…