@Inbook{Schiffl2020,
author="Schiffl, Jonas
and Ahrendt, Wolfgang
and Beckert, Bernhard
and Bubel, Richard",
editor="Ahrendt, Wolfgang
and Beckert, Bernhard
and Bubel, Richard
and H{\"a}hnle, Reiner
and Ulbrich, Mattias",
title="Formal Analysis of Smart Contracts: Applying the KeY System",
bookTitle="Deductive Software Verification: Future Perspectives: Reflections on the Occasion of 20 Years of KeY",
year="2020",
publisher="Springer International Publishing",
address="Cham",
pages="204--218",
abstract="Smart contracts are programs running on decentralized, distributed ledger platforms. Rigorous formal analysis of these programs is highly desirable because they manage valuable assets and therefore are a prime target for security attacks. In this paper, we show that the computation model of smart contracts allows the application of formal methods designed for analysing single-threaded imperative programs. We discuss different classes of correctness properties and the formal methods that may be applied. Furthermore, we show how deductive program verification in particular can be used to prove correctness of smart contracts, and we discuss two approaches where we have applied the program verification tool KeY.",
isbn="978-3-030-64354-6",
doi="10.1007/978-3-030-64354-6_8",
url="https://doi.org/10.1007/978-3-030-64354-6_8"
}