Specifying Framing Conditions for Smart Contracts

@inproceedings{beckert_specifying_2020,
	location = {Cham},
	title = {Specifying Framing Conditions for Smart Contracts},
	isbn = {978-3-030-61467-6},
	abstract = {Smart contracts are programs which run in conjunction with distributed ledgers.
                    They often manage valuable assets, but, like all programs, they contain errors
                    which can be exploited by an attacker. This makes them are a prime target for
                    formal methods. Many formal analysis methods require the contracts' program code
                    to be annotated with formal specifications. In this paper, we propose an approach
                    and a formalism to enrich specifications with frame conditions, i.e., a
                    specification of what a smart contract function cannot resp. will not do. We
                    discuss the storage models of two smart contract platforms, Ethereum and
                    Hyperledger Fabric, and propose languages for specifying frame conditions for
                    both of them, based on the theory of dynamic frames.},
	pages = {43--59},
	booktitle = {ISoLA 2020: Leveraging Applications of Formal Methods, Verification and Validation},
	publisher = {Springer International Publishing},
	author = {Bernhard Beckert and Jonas Schiffl},
	editor = {Tiziana Margaria and Bernhard Steffen},
	year = {2020},
        month = oct
}