- This event has passed.
Mooly Sagiv on Formally Verifying Smart Contracts
March 25 @ 6:00 PM - 9:00 PMFree
We’re pleased to have Professor Mooly Sagiv  from Tel Aviv University and the Vmware Research Group speak to us on formal verification of smart contracts. We will begin the event with a short talk from Eric McCarthy  of the Kestrel Institute on how ACL2  could be used to verify the EVM.
Mooly’s abstract: “Smart contracts define transactions to be executed on top of Blockchain technology. The combination of a decentralized secure computation platform provided by blockchains, and the rich expressiveness of smart contracts, allows us to automate and secure processes which today are manual, slow, inefficient and prone to forgery. However, smart contracts are vulnerable to software errors which are exploited, e.g., for money thefts. In the last 18 months, there were 3 high-impact (over $500M) incidents caused directly by buggy smart contracts that were either exploited maliciously or mistakenly compromised.”
“I will present a high level overview of two techniques which can be used for early detection of contract vulnerabilities and preventing them by combining compile-time and run-time techniques: deductive verification and runtime checking.”
Mooly is co-author on the work that Yan Michalevsky presented to us recently . http://www.cs.tau.ac.il/~msagiv/