Program
July 20, 6:00 AM - 8:00 AM PDT (UTC-7)
6:00-6:05 Introduction
6:05-7:00 Invited talk
- Formal Design, Implementation and Verification of Blockchain Languages using K, Grigore Rosu
Abstract: The usual post-mortem approach to formal language semantics and verification, where the language is firstly implemented and used in production for many years before a need for formal semantics and verification tools naturally arises, simply does not work anymore. New blockchain languages or virtual machines are proposed at an alarming rate, followed by new versions of them every few weeks, together with programs (or smart contracts) in these languages that are responsible for financial transactions of potentially significant value. Formal analysis and verification tools are therefore needed immediately for such languages and virtual machines. We will present recent academic and commercial results in developing blockchain languages and virtual machines that come directly equipped with formal analysis and verification tools. The main idea is to generate all these automatically, correct-by-construction from a formal language specification.
Bio: Grigore Rosu is a professor in the Department of Computer Science at the University of Illinois at Urbana-Champaign (UIUC), where he leads the Formal Systems Laboratory (FSL), and the founder of Runtime Verification, Inc (RV). His research interests encompass both theoretical foundations and system development in the areas of formal methods, software engineering and programming languages. Before joining UIUC in 2002, he was a research scientist at NASA Ames. He obtained his Ph.D. at the University of California at San Diego in 2000. He was offered the CAREER award by the NSF, the Dean’s award for excellence in research by the College of Engineering at UIUC in 2014, and the outstanding junior award by the Computer Science Department at UIUC in 2005. He won the ASE IEEE/ACM most influential paper award in 2016 (for an ASE 2001 paper) and the RV test of time award (for an RV 2001 paper) for papers that helped shape the runtime verification field, the ACM SIGSOFT distinguished paper awards at ASE 2008, ASE 2016, and OOPSLA 2016, and the best software science paper award at ETAPS 2002.
7:05-8:00 Smart contracts and payments
5 min short presentation + 5 min Q&A for each talk. 15 min breakout time for follow-up discussions with speakers in separate rooms.
- A Blockchain Model in Tamarin, Shuang Wu, Kristian Gjøsteen and Colin Alexander Boyd
- Tezla, an intermediate representation for static analysis of Michelson smart contracts, João Santos Reis, Paul Crocker and Simão Melo de Sousa
- Populating the Peephole Optimizer of a Smart Contract Compiler, Maria A Schett and Julian Nagele
- Formal Specification and Verification of Solidity Contracts with Events, Ákos Hajdu, Dejan Jovanović and Gabriela Ciocarlie
July 21, 5:45 AM - 8:00 AM PDT (UTC-7)
5:45-6:30 Merkle trees and Bitcoin
5 min short presentation + 5 min Q&A for each talk. 15 min breakout time for follow-up discussions with speakers in separate rooms.
- Authenticated Data Structures as Functors in Isabelle/HOL, Andreas Lochbihler and Ognjen Maric
- Mechanized Formal Model of the Bitcoin’s Blockchain Validation Procedures, Kristijan Rupić, Lovro Rozic and Ante Derek
- Towards Verifying the Bitcoin-S Library, Kai Brünnler, Ramon Boss and Anna Doukmak
6:30-7:15 Consensus
5 min short presentation + 5 min Q&A for each talk. 15 min breakout time for follow-up discussions with speakers in separate rooms.
- Formal verification of the Stellar Consensus Protocol, Giuliano Losa and Mike Dodds
- Formal Specification and Model Checking of the Tendermint Blockchain Synchronization Protocol, Sean Braithwaite, Ethan Buchman, Igor Konnov, Zarko Milosevic, Ilina Stoilkovska, Josef Widder and Anca Zamfir
- Inter-blockchain protocols with the Isabelle Infrastructure framework, Florian Kammueller and Uwe Nestmann
7:15-8:00 Lightning talks
3 min short presentation + 3 min Q&A for each talk. 15 min breakout time for follow-up discussions with speakers in separate rooms.
- Verifying, testing and running smart contracts in ConCert, Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen and Bas Spitters
- Summary of Bitcoin Trace-Net: Formal Contract Verification at Signing Time, James Chiang
- High-assurance field inversion for pairing-friendly primes, Benjamin S. Hvass, Diego F. Aranha and Bas Spitters
- Albert, an intermediate smart-contract language for Tezos, Bruno Bernardo, Raphaël Cauderlier, Arvid Jakobsson, Basile Pesin and Julien Tesson
- WhylSon: Proving your Michelson Smart Contracts in Why3, Luís Pedro Arrojado Horta, João Santos Reis, Mário Pereira and Simão Melo de Sousa