PROGRAM
Friday, October 11th
View this program: with abstractssession overviewtalk overview
09:05-10:00 Session 2: Keynote
| 09:05 | The Scilla Journey: from Proof General to Thousands of Nodes (abstract) |
10:30-12:30 Session 3: Smart Contracts 1
Chair:
| 10:30 | Smart Contracts: Application Scenarios for Deductive Program Verification (abstract) |
| 11:00 | Deductive Proof of Industrial Smart Contracts Using Why3 (abstract) |
| 11:30 | Verifying Smart Contracts with Cubicle (abstract) |
| 12:00 | Call me Back, I have a Type Invariant (abstract) |
14:00-15:30 Session 4: Verifying Consensus
Chair:
| 14:00 | Statistical Model Checking of RANDAO's Resilience to Pre-computed Reveal Strategies (abstract) |
| 14:30 | A Distributed Blockchain Model of Selfish Mining (abstract) |
| 15:00 | Towards a Verified Model of the Algorand Consensus Protocol in Coq (abstract) |
16:00-18:00 Session 5: Smart Contracts 2
Chair:
| 16:00 | Solidity 0.5: when typed does not mean type safe (abstract) |
| 16:15 | Towards a Smart Contract Verification Framework in Coq (abstract) |
| 16:30 | Mi-Cho-Coq, a framework for certifying Tezos Smart Contracts (abstract) |
| 17:00 | Smart Contract Interactions in Coq (abstract) |
| 17:30 | Formal specification of a security framework for smart contracts (abstract) |