Smart Contracts: Application Scenarios for Deductive Program Verification

@inproceedings{schiffl_smart_2019,
    title     = {Smart Contracts: Application Scenarios for Deductive Program Verification},
    author    = {Bernhard Beckert and Jonas Schiffl and Mattias Ulbrich},
    editor    = {Bruno Bernardo and N\'{e}stor Cata\~{n}o and Diego Marmsoler},
    booktitle = {1st Workshop on Formal Methods for Blockchains ({FMBC} 2019)
                 hosted by the 3rd Formal Methods World Congress ({FM}’19)},
    month     = oct,
    year      = {2019},
    abstract  = {Smart contracts are programs that run on a distributed ledger platform.                
                 They usually manage resources representing valuable
                 assets. Moreover, their source code is visible to potential
                 attackers, they are distributed, and bugs are hard to
                 fix. Thus, they are susceptible to attacks exploiting programming errors.
                 Their vulnerability makes a rigorous formal analysis of the functional
                 correctness of smart contracts highly desirable.

                 In this short paper, we show that the architecture of smart
                 contract platforms offers a computation model for smart
                 contracts that yields itself naturally to deductive program
                 verification. We discuss different classes of correctness
                 properties of distributed ledger applications, and show that
                 design-by-contract verification tools are suitable to prove
                 these properties. We present experiments where we apply the
                 \KeY verification tool to smart contracts in the Hyperledger
                 Fabric framework which are implemented in Java and 
                 specified using the Java Modeling Language.},
    venue     = {Porto, Portugal},
    eventdate = {2019-10-11/2019-10-11}
}