PROGRAM
Sunday, April 7th
View this program: with abstractssession overviewtalk overview
09:00-10:00 Session 1: Keynote
| 09:00 | Welcome |
| 09:05 | Deductive verification of smart contracts (abstract) |
10:30-12:20 Session 2: Consensus
| 10:30 | Towards Formal Verification of DAG-Based Blockchain Consensus Protocols (abstract) |
| 10:50 | Formal specification of the Cardano blockchain ledger, mechanized in Agda (abstract) |
| 11:20 | Formally Verifying Safety of Chained Moonshot Consensus protocol (abstract) |
| 11:50 | Towards Mechanised Consensus in Isabelle (abstract) |
14:00-15:50 Session 3: Smart Contracts 1
| 14:00 | Secure Smart Contracts with Isabelle/Solidity (abstract) |
| 14:20 | Formalizing Automated Market Makers in the Lean 4 Theorem Prover (abstract) |
| 14:50 | Towards Benchmarking of Solidity verification tools (abstract) |
| 15:20 | Towards Formally Specifying and Verifying Smart Contract Upgrades in Coq (abstract) |
16:30-18:05 Session 4: Smart Contracts 2
| 16:30 | A Practical Notion of Liveness in Smart Contract Applications (abstract) |
| 17:00 | Securing Aptos Framework with Formal Verification (abstract) |
| 17:30 | Structured Contracts in the EUTxO Ledger Model (abstract) |
| 18:00 | Wrap up |