Mon 8 Jan 2018 14:00 - 14:30 at Museum A - Verified Applications Chair(s): K. Rustan M. Leino

Blockchain technology has increasing attention in research and across many industries.
The Ethereum blockchain offers smart contracts, which are small programs defined,
executed, and recorded as transactions in the blockchain transaction history.
These smart contracts run on the Ethereum Virtual Machine (EVM) and can be used to encode
agreements, transfer assets, and enforce integrity conditions in relationships between parties.
Smart contracts can carry financial value, and are increasingly
used for safety-, security-, or mission-critical purposes.
Errors in smart contracts have led and will lead to loss or harm.
Formal verification can provide the highest level of confidence about the
correct behaviour of smart contracts.
In this paper we extend an existing EVM formalisation in Isabelle/HOL by a sound
program logic at the level of bytecode.
We structure bytecode sequences into blocks of straight-line
code and create a program logic to reason about these.
This abstraction is a step towards control of the cost and complexity of formal verification
of EVM smart contracts.

Mon 8 Jan
Times are displayed in time zone: (GMT-07:00) Tijuana, Baja California change

13:30 - 15:30: CPP 2018 - Verified Applications at Museum A
Chair(s): K. Rustan M. LeinoAmazon
CPP-201813:30 - 14:00
Conrad WattUniversity of Cambridge, UK
CPP-201814:00 - 14:30
Sidney AmaniUNSW, Australia, Myriam BégelENS Paris-Saclay, France, Maksym Bortin, Mark StaplesCSIRO, Australia
CPP-201814:30 - 15:00
George PîrleaUniversity College London, Ilya SergeyUniversity College London
DOI Pre-print
CPP-201815:00 - 15:30
Cezary KaliszykUniversity of Innsbruck, Julian ParsertUniversity of Innsbruck, Austria