Date |
Lesson # |
Lecturer(s) |
Paper(s) |
16.03.25
|
1 |
Yoni |
Introduction
slides
|
23.03.25
|
2 |
Guy and Oz
|
A survey of attacks on Ethereum smart contracts
slides
|
30.03.25
|
3 |
Shira and Or L
|
Proof-Carrying Smart Contracts
|
06.04.25
|
4 |
Avinoam and Khaled
|
Demystifying Loops in Smart Contracts
|
13.04.25
|
-- |
|
Passover
|
20.04.25
|
-- |
|
Passover
|
27.04.25
|
5 |
Sharon and Nadav
|
Chapters 1.1 -- 1.3, 2.1 -- 2.3, 3.1 -- 3.6 in the book "The Calculus of Computation"
|
04.05.25
|
6 |
Sapir and Roy Mo
|
Chapters 12.1 -- 12.3 in the book "Decision Procedures: An Algorithmic Point of View"
|
11.05.25
|
7 |
Dolev and Roy Ma
|
Securing Aptos Framework with Formal Verification
|
18.05.25
|
8 |
Evyatar and Avichai
|
SMT-Friendly Formalization of the Solidity Memory Model
|
25.05.25
|
9 |
Or H and Orel
|
SolCMC: Solidity Compiler's Model Checker
|
01.06.25
|
-- |
|
SHAVUOT
|
08.06.25
|
10 |
Omri and Michael
|
Move: A Language With Programmable Resources. Blackshear et al.
|
15.06.25
|
11 |
Sandos and Muhammad
|
Overapproximation of Non-linear Integer Arithmetic for Smart Contract Verification
|
22.06.25
|
12 |
Elia and Or S
|
Accurate Smart Contract Verification through Direct Modelling
|
29.06.25
|
13 |
Bar and Shaked
|
Formal Verification of Workflow Policies for Smart Contracts in Azure Blockchain
|