PROGRAM
Days: Monday, July 20th Tuesday, July 21st
Monday, July 20th
View this program: with abstractssession overviewtalk overview
06:05-07:00 Session 2: Invited talk
| 06:05 | Formal Design, Implementation and Verification of Blockchain Languages using K (abstract) |
07:05-08:00 Session 3: Smart contracts and payments
| 07:05 | Formal Specification and Verification of Solidity Contracts with Events (short paper) (abstract) |
| 07:15 | Populating the Peephole Optimizer of a Smart Contract Compiler (abstract) |
| 07:25 | Tezla, an intermediate representation for static analysis of Michelson smart contracts (abstract) |
| 07:35 | A Blockchain Model in Tamarin (abstract) |
Tuesday, July 21st
View this program: with abstractssession overviewtalk overview
05:45-06:30 Session 4: Merkle trees and Bitcoin
| 05:45 | Authenticated Data Structures as Functors in Isabelle/HOL (abstract) |
| 05:55 | Mechanized Formal Model of the Bitcoin's Blockchain Validation Procedures (abstract) |
| 06:05 | Towards Verifying the Bitcoin-S Library (abstract) |
06:30-07:15 Session 5: Consensus
| 06:30 | Formal verification of the Stellar Consensus Protocol (abstract) |
| 06:40 | Formal Specification and Model Checking of the Tendermint Blockchain Synchronization Protocol (Short Paper) (abstract) |
| 06:50 | Inter-blockchain protocols with the Isabelle Infrastructure framework (abstract) |
07:15-08:00 Session 6: Lightning talks
| 07:15 | Verifying, testing and running smart contracts in ConCert (abstract) |
| 07:21 | Summary of Bitcoin Trace-Net: Formal Contract Verification at Signing Time. (Extended Abstract) (abstract) |
| 07:27 | High-assurance field inversion for pairing-friendly primes (abstract) |
| 07:33 | Albert, an intermediate smart-contract language for Tezos. (abstract) |
| 07:39 | WhylSon: Proving your Michelson Smart Contracts in Why3 (abstract) |