41 citations · 92 across the 8 of their papers we have counts for
8 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…
Formalising Decentralised Exchanges in Coq
Eske Hoy Nielsen, Danil Annenkov, Bas Spitters
The number of attacks and accidents leading to significant losses of crypto-assets is growing. According to Chainalysis, in 2021, approx. $14 billion has been lost due to various i…
Certified Compilation of Financial Contracts
Danil Annenkov, Martin Elsman
We present an extension to a certified financial contract management system that allows for templated declarative financial contracts and for integration with financial stochastic…
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.…
ConCert: A Smart Contract Certification Framework in Coq
Danil Annenkov, Jakob Botsch Nielsen, Bas Spitters
We present a new way of embedding functional languages into the Coq proof assistant by using meta-programming. This allows us to develop the meta-theory of the language using the d…