9 citations · 9 across the 3 of their papers we have counts for
3 papers
Finding smart contract vulnerabilities with ConCert's property-based testing framework
Mikkel Milo, Eske Hoy Nielsen, Danil Annenkov +1
We provide three detailed case studies of vulnerabilities in smart contracts, and show how property-based testing would have found them: 1. the Dexter1 token exchange; 2. the iToke…
Extracting functional programs from Coq, in Coq
Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen +1
We implement extraction of Coq programs to functional languages based on MetaCoq's certified erasure. We extend the MetaCoq erasure output language with typing information and use…
Extracting Smart Contracts Tested and Verified in Coq
Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen +1
We implement extraction of Coq programs to functional languages based on MetaCoq's certified erasure. As part of this, we implement an optimisation pass removing unused arguments.…