Joshua Sunshine

Smarter Smart Contract Development Tools

2019

Much recent work focuses on finding bugs and security vulnerabilities in smart contracts written in existing languages. Although this approach may be helpful, it does not address flaws in the underlying programming language, which can …

Gradual C0: Symbolic Execution for Gradual Verification

2024 · ACM Transactions on Programming Languages and Systems

Current static verification techniques such as separation logic support a wide range of programs. However, such techniques only support complete and detailed specifications, which places an undue burden on users. To solve this problem, prior …