Research Commons
      • Browse 
        • Communities & Collections
        • Titles
        • Authors
        • By Issue Date
        • Subjects
        • Types
        • Series
      • Help 
        • About
        • Collection Policy
        • OA Mandate Guidelines
        • Guidelines FAQ
        • Contact Us
      • My Account 
        • Sign In
        • Register
      View Item 
      •   Research Commons
      • University of Waikato Research
      • Computing and Mathematical Sciences
      • Computing and Mathematical Sciences Papers
      • View Item
      •   Research Commons
      • University of Waikato Research
      • Computing and Mathematical Sciences
      • Computing and Mathematical Sciences Papers
      • View Item
      JavaScript is disabled for your browser. Some features of this site may not work without it.

      Provably correct smart contracts: An approach using DeepSEA

      Britten, Daniel; Sjöberg, Vilhelm; Reeves, Steve
      Thumbnail
      Files
      SPLASH_2022.pdf
      Accepted version, 387.5Kb
      DOI
       10.1145/3563768.3564116
      Find in your library  
      Permanent link to Research Commons version
      https://hdl.handle.net/10289/15471
      Abstract
      It is possible to download a piece of software over the internet and then verify its correctness locally using an appropriate trusted proof system. However, on a blockchain like Ethereum, smart contracts cannot be altered once deployed. This guarantee of immutability makes it possible for end users to interact collectively with a 'networked' piece of software, with the same opportunity to verify its correctness. Formal verification of smart contracts on a blockchain therefore offers an unprecedented opportunity for end users to collectively interact with a deployed instance of software that they can verify while not relying on a central authority. All that is required to be trusted beyond the blockchain itself is an appropriate proof system, a component which always needs to be in the trusted computing base, and whose rules and definitions can be public knowledge. DeepSEA (Deep Simulation of Executable Abstractions) could serve as such a proof system.
      Date
      2022
      Type
      Conference Contribution
      Publisher
      Association for Computing Machinery
      Rights
      This is an author’s accepted version of a conference paper published in SPLASH Companion 2022: Companion Proceedings of the 2022 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity. © 2022 Copyright held by the authors. Publication rights licensed to ACM.
      Collections
      • Computing and Mathematical Sciences Papers [1455]
      Show full item record  

      Usage

       
       
       

      Usage Statistics

      For this itemFor all of Research Commons

      The University of Waikato - Te Whare Wānanga o WaikatoFeedback and RequestsCopyright and Legal Statement