Papers (113)

#Title
Citations
1.Formal verification of smart contracts: Short paper Bhargavan, Karthikeyan and Delignat-Lavaud, Antoine and Fournet, C\'edric and Gollamudi, Anitha and Gonthier, Georges and Kobeissi, Nadim and Kulatova, Natalia and Rastogi, Aseem and Sibut-Pinote, Thomas and Swamy, Nikhil and others. 2016
550
2.Securify: Practical security analysis of smart contracts Tsankov, Petar and Dan, Andrei and Drachsler-Cohen, Dana and Gervais, Arthur and Buenzli, Florian and Vechev, Martin. 2018
481
3.Defining the ethereum virtual machine for interactive theorem provers Hirai, Yoichi. 2017
265
4.A Semantic Framework for the Security Analysis of Ethereum smart contracts Grishchenko, Ilya and Maffei, Matteo and Schneidewind, Clara. 2018
247
5.Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL Amani, Sidney and B\'egel, Myriam and Bortin, Maksym and Staples, Mark. 2018
211
6.Designing secure Ethereum smart contracts: A finite state machine based approach Mavridou, Anastasia and Laszka, Aron. 2017
173
7.VerX: Safety Verification of Smart Contracts Permenev, Anton and Dimitrov, Dimitar and Tsankov, Petar and Drachsler-Cohen, Dana and Vechev, Martin. 2019
119
8.A concurrent perspective on smart contracts Sergey, Ilya and Hobor, Aquinas. 2017
111
9.Validation of decentralised smart contracts through game theory and formal methods Bigi, Giancarlo and Bracciali, Andrea and Meacci, Giovanni and Tuosto, Emilio. 2015
105
10.Formal verification of smart contracts based on users and blockchain behaviors models Abdellatif, Tesnim and Brousmiche, Kei-L\'eo. 2018
105
11.Scilla: a Smart Contract Intermediate-Level LAnguage Sergey, Ilya and Kumar, Amrit and Hobor, Aquinas. 2018
93
12.Simplicity: A new language for blockchains O'Connor, Russell. 2017
90
13.KEVM: A Complete Semantics of the Ethereum Virtual Machine Hildenbrandt, Everett and Saxena, Manasvi and Zhu, Xiaoran and Rodrigues, Nishant and Daian, Philip and Guth, Dwight and Rosu, Grigore. 2017
86
14.A formal verification tool for Ethereum VM Bytecode Park, Daejun and Zhang, Yi and Saxena, Manasvi and Daian, Philip and Ro\csu, Grigore. 2018
82
15.EthIR: A Framework for High-Level Analysis of Ethereum Bytecode Albert, Elvira and Gordillo, Pablo and Livshits, Benjamin and Rubio, Albert and Sergey, Ilya. 2018
80
16.VeriSolid: Correct-by-Design Smart Contracts for Ethereum Mavridou, Anastasia and Laszka, Aron and Stachtiari, Emmanouela and Dubey, Abhishek. 2019
74
17.Towards safer smart contracts: A survey of languages and verification methods Harz, Dominik and Knottenbelt, William. 2018
70
18.Mechanising Blockchain Consensus P\^\irlea, George and Sergey, Ilya. 2018
67
19.Exploiting the laws of order in smart contracts Kolluri, Aashish and Nikolic, Ivica and Sergey, Ilya and Hobor, Aquinas and Saxena, Prateek. 2019
64
20.Safer smart contract programming with Scilla Sergey, Ilya and Nagaraj, Vaivaswatha and Johannsen, Jacob and Kumar, Amrit and Trunov, Anton and Hao, Ken Chan Guan. 2019
62
21.solc-verify: A Modular Verifier for Solidity Smart Contracts Hajdu, \'Akos and Jovanovi\'c, Dejan. 2019
61
22.Raziel: private and verifiable smart contracts on blockchains S\'anchez, David Cerezo. 2018
56
23.Model-Checking of Smart Contracts Nehai, Zeinab and Piriou, Pierre-Yves and Daumas, Frederic. 2018
54
24.Modeling bitcoin contracts by timed automata Andrychowicz, Marcin and Dziembowski, Stefan and Malinowski, Daniel and Mazurek, \Lukasz. 2014
49
25.Smt-based verification of solidity smart contracts Alt, Leonardo and Reitwiessner, Christian. 2018
49
26.VeriSmart: A Highly Precise Safety Verifier for Ethereum Smart Contracts So, Sunbeom and Lee, Myungho and Park, Jisu and Lee, Heejo and Oh, Hakjoo. 2019
45
27.Marlowe: Financial contracts on blockchain Seijas, Pablo Lamela and Thompson, Simon. 2018
39
28.Smart contracts and opportunities for formal methods Miller, Andrew and Cai, Zhicheng and Jha, Somesh. 2018
32
29.eThor: Practical and Provably Sound Static Analysis of Ethereum Smart Contracts Schneidewind, Clara and Grishchenko, Ilya and Scherer, Markus and Maffei, Matteo. 2020
29
30.Temporal Properties of Smart Contracts Sergey, Ilya and Kumar, Amrit and Hobor, Aquinas. 2018
28
31.Monitoring smart contracts: Contractlarva and open challenges beyond Azzopardi, Shaun and Ellul, Joshua and Pace, Gordon J. 2018
28
32.Formal Specification and Verification of Smart Contracts for Azure Blockchain Lahiri, Shuvendu K and Chen, Shuo and Wang, Yuepeng and Dillig, Isil. 2018
22
33.Developing secure Bitcoin contracts with BitML Atzei, Nicola and Bartoletti, Massimo and Lande, Stefano and Yoshida, Nobuko and Zunino, Roberto. 2019
20
34.A Comprehensive Survey on Smart Contract Construction and Execution: Paradigms, Tools and Systems Hu, Bin and Zhang, Zongyang and Liu, Jianwei and Liu, Yizhong and Yin, Jiayuan and Lu, Rongxing and Lin, Xiaodong. 2020
20
35.Mi-Cho-Coq, a framework for certifying Tezos Smart Contracts Bernardo, Bruno and Cauderlier, Rapha\"el and Hu, Zhenlei and Pesin, Basile and Tesson, Julien. 2019
19
36.Domain Specific Language for Smart Contract Development W\"ohrer, Maximilian and Zdun, Uwe. 2020
19
37.A Survey of Smart Contract Formal Specification and Verification Tolmach, Palina and Li, Yi and Lin, Shang-Wei and Liu, Yang and Li, Zengxiang. 2020
19
38.What are the Actual Flaws in Important Smart Contracts (and How Can We Find Them)? Groce, Alex and Feist, Josselin and Grieco, Gustavo and Colburn, Michael. 2019
18
39.SAFEVM: A Safety Verifier for Ethereum Smart Contracts Albert, Elvira and Correas, Jes\'us and Gordillo, Pablo and Rom\'an-D\'\iez, Guillermo and Rubio, Albert. 2019
17
40.A minimal core calculus for Solidity contracts Bartoletti, Massimo and Galletta, Letterio and Murgia, Maurizio. 2019
16
41.IELE: a rigorously designed language and tool ecosystem for the blockchain Kasampalis, Theodoros and Guth, Dwight and Moore, Brandon and Șerb\uanuț\ua, Traian Florin and Zhang, Yi and Filaretti, Daniele and Șerb\uanuț\ua, Virgil and Johnson, Ralph and Ro\csu, Grigore. 2019
16
42.A minimal core calculus for Solidity contracts Bartoletti, Massimo and Galletta, Letterio and Murgia, Maurizio. 2019
16
43.Automated Verification of Electrum Wallet Mathieu Turuani and Thomas Voegtlin and Micha\"el Rusinowitch. 2016
15
44.ConCert: A Smart Contract Certification Framework in Coq Annenkov, Danil and Nielsen, Jakob Botsch and Spitters, Bas. 2020
14
45.ConCert: a smart contract certification framework in Coq Annenkov, Danil and Nielsen, Jakob Botsch and Spitters, Bas. 2020
14
46.Smart Contract Interactions in Coq Nielsen, Jakob Botsch and Spitters, Bas. 2019
13
47.Executable Operational Semantics of Solidity Jiao, Jiao and Kan, Shuanglong and Lin, Shang-Wei and Sanan, David and Liu, Yang and Sun, Jun. 2018
11
48.Towards a formally verified implementation of the MimbleWimble cryptocurrency protocol Betarte, Gustavo and Cristi\'a, Maximiliano and Luna, Carlos and Silveira, Adri\'an and Zanarini, Dante. 2019
10
49.Functional blockchain contracts Chakravarty, Manuel and Kireev, Roman and MacKenzie, Kenneth and McHale, Vanessa and M\"uller, Jann and Nemish, Alexander and Nester, Chad and Jones, Michael Peyton and Thompsona, Simon and Valentine, Rebecca and others. 2019
10
50.Unraveling recursion: compiling an IR with recursion to system F Jones, Michael Peyton and Gkoumas, Vasilis and Kireev, Roman and MacKenzie, Kenneth and Nester, Chad and Wadler, Philip. 2019
9
51.MPro: Combining Static and Symbolic Analysis for Scalable Testing of Smart Contract Zhang, William and Banescu, Sebastian and Pasos, Leodardo and Stewart, Steven and Ganesh, Vijay. 2019
9
52.Albert, an intermediate smart-contract language for the Tezos blockchain Bernardo, Bruno and Cauderlier, Rapha\"el and Pesin, Basile and Tesson, Julien. 2020
9
53.Native Custom Tokens in the Extended UTXO Model Chakravarty, Manuel MT and Chapman, James and MacKenzie, Kenneth and Melkonian, Orestis and M\"uller, Jann and Jones, Michael Peyton and Vinogradova, Polina and Wadler, Philip. 2020
8
54.Formal Specification and Model Checking of the Tendermint Blockchain Synchronization Protocol (Short Paper) Braithwaite, Sean and Buchman, Ethan and Konnov, Igor and Milosevic, Zarko and Stoilkovska, Ilina and Widder, Josef and Zamfir, Anca. 2020
8
55.Compositional Security for Reentrant Applications Cecchetti, Ethan and Yao, Siqiu and Ni, Haobin and Myers, Andrew C. 2021
8
56.Practical Smart Contract Sharding with Ownership and Commutativity Analysis P\^\irlea, George and Kumar, Amrit and Sergey, Ilya. 2021
8
57.Formal Analysis of Composable DeFi Protocols Tolmach, Palina and Li, Yi and Lin, Shang-Wei and Liu, Yang. 2021
8
58.Temporal aspects of smart contracts for financial derivatives Clack, Christopher D and Vanca, Gabriel. 2018
8
59.Contingent payments on a public ledger: models and reductions for automated verification. Bursuc, Sergiu and Kremer, Steve. 2019
6
60.Proof-Carrying Smart Contracts Dickerson, Thomas and Gazzillo, Paul and Herlihy, Maurice and Saraph, Vikram and Koskinen, Eric. 2018
6
61.Analyzing Smart Contracts: From EVM to a sound Control-Flow Graph Albert, Elvira and Correas, Jes\'us and Gordillo, Pablo and Rom\'an-D\'\iez, Guillermo and Rubio, Albert. 2020
6
62.SmartBugs: A Framework to Analyze Solidity Smart Contracts Ferreira, Jo\~ao F and Cruz, Pedro and Durieux, Thomas and Abreu, Rui. 2020
6
63.Extracting Smart Contracts Tested and Verified in Coq Annenkov, Danil and Milo, Mikkel and Nielsen, Jakob Botsch and Spitters, Bas. 2020
6
64.Cross-Chain Payment Protocols with Success Guarantees van Glabbeek, Rob and Gramoli, Vincent and Tholoniat, Pierre. 2019
5
65.Formalising and verifying smart contracts with Solidifier: a bounded model checker for Solidity Antonino, Pedro and Roscoe, AW. 2020
5
66.Renegotiation and recursion in Bitcoin contracts Bartoletti, Massimo and Murgia, Maurizio and Zunino, Roberto. 2020
5
67.Smart Contract modeling and verification techniques: A survey Imeri, Adnan and Agoulmine, Nazim and Khadraoui, Djamel. 2020
5
68.Blockchains as kripke models: An analysis of atomic cross-chain swap Hirai, Yoichi. 2018
5
69.Clockwork Finance: Automated Analysis of Economic Security in Smart Contracts Kushal Babel and Philip Daian and Mahimna Kelkar and Ari Juels. 2021
5
70.WIP: Finding Bugs Automatically in Smart Contracts with Parameterized Invariants Bernardi, Thomas and Dor, Nurit and Fedotov, Anastasia and Grossman, Shelly and Immerman, Neil and Jackson, Daniel and Nutz, Alex and Oppenheim, Lior and Pistiner, Or and Rinetzky, Noam and others. 2020
4
71.Flexible Formality Practical Experience with Agile Formal Methods Szamotulski, Marcin and Vinogradova, Polina. 2020
4
72.Formal security analysis of MPC-in-the-head zero-knowledge protocols Nikolaj Sidorenco and Sabine Oechsner and Bas Spitters. 2021
4
73.Termination of Ethereum's Smart Contracts Genet, Thomas and Jensen, Thomas and Sauvage, Justine. 2020
3
74.Tezla, an Intermediate Representation for Static Analysis of Michelson Smart Contracts Santos Reis, Jo\~ao and Crocker, Paul and Melo de Sousa, Sim\~ao. 2020
3
75.WhylSon: Proving your Michelson Smart Contracts in Why3 da Horta, Lu\'\is Pedro Arrojado and Reis, Jo\~ao Santos and Pereira, M\'ario and de Sousa, Sim\~ao Melo. 2020
3
76.A formal model of Algorand smart contracts Bartoletti, Massimo and Bracciali, Andrea and Lepore, Cristian and Scalas, Alceste and Zunino, Roberto. 2020
3
77.A Tendermint Light Client Braithwaite, Sean and Buchman, Ethan and Khoffi, Ismail and Konnov, Igor and Milosevic, Zarko and Ruetschi, Romain and Widder, Josef. 2020
3
78.The Good, The Bad and The Ugly: Pitfalls and Best Practices in Automated Sound Static Analysis of Ethereum Smart Contracts Schneidewind, Clara and Scherer, Markus and Maffei, Matteo. 2020
3
79.Towards declarative smart contracts Purnell, Kevin and Schwitter, Rolf. 2019
2
80.Formal Verification of Solidity contracts in Event-B Zhu, Jian and Hu, Kai and Filali, Mamoun and Bodeveix, Jean-Paul and Talpin, Jean-Pierre. 2020
2
81.Formal Specification and Verification of Solidity Contracts with Events Hajdu, Akos and Jovanovic, Dejan and Ciocarlie, Gabriela. 2020
2
82.Formalizing Nakamoto-Style Proof of Stake Søren Eller Thomsen and Bas Spitters. 2020
2
83.SmartPulse: Automated Checking of Temporal Properties in Smart Contracts Stephens, Jon and Ferles, Kostas and Mariano, Benjamin and Lahiri, Shuvendu and Dillig, Isil. 2021
2
84.Model Checking Bitcoin and other Proof-of-Work Consensus Protocols DiGiacomo-Castillo, Max and Liang, Yiyun and Pal, Advay and Mitchell, John C. 2020
1
85.Making Tezos Smart Contracts More Reliable with Coq Bernardo, Bruno and Cauderlier, Rapha\"el and Claret, Guillaume and Jakobsson, Arvid and Pesin, Basile and Tesson, Julien. 2020
1
86.LEO: A Programming Language for Formally Verified,Zero-Knowledge Applications Collin Chin and Howard Wu and Raymond Chu and Alessandro Coglio and Eric McCarthy and Eric Smith. 2021
1
87.SAILFISH: Vetting Smart Contract State-Inconsistency Bugs in Seconds Bose, Priyanka and Das, Dipanjan and Chen, Yanju and Feng, Yu and Kruegel, Christopher and Vigna, Giovanni. 2021
1
88.Verification of a Merkle Patricia Tree Library Using F Sato, Sota and Banno, Ryotaro and Furuse, Jun and Suenaga, Kohei and Igarashi, Atsushi. 2021
1
89.Rich specifications for Ethereum smart contract verification Br\"am, Christian and Eilers, Marco and M\"uller, Peter and Sierra, Robin and Summers, Alexander J. 2021
1
90.On the specification and verification of atomic swap smart contracts⋆ van der Meyden, Ron. 2018
0
91.Formal verification of Deed contract in Ethereum name service Hirai, Yoichi. 2016
0
92.Toychain: Formally Verified Blockchain Consensus George P\^ırlea. 2019
0
93.Formal specification of a security framework for smart contracts Mandrykin, Mikhail and O'Shannessy, Jake and Payne, Jacob and Shchepetkov, Ilya. 2020
0
94.An Empirical Study of Ownership, Typestate, and Assets in the Obsidian Smart Contract Language Coblenz, Michael and Aldrich, Jonathan and Sunshine, Joshua and Myers, Brad. 2020
0
95.UTXOma: UTXO with Multi-Asset Support Chakravarty, Manuel MT and Chapman, James and MacKenzie, Kenneth and Melkonian, Orestis and M\"uller, Jann and Jones, Michael Peyton and Vinogradova, Polina and Wadler, Philip and Zahnentferner, Joachim. 2020
0
96.Compiling a Higher-Order Smart Contract Language to LLVM Nagaraj, Vaivaswatha and Johannsen, Jacob and Trunov, Anton and P\^\irlea, George and Kumar, Amrit and Sergey, Ilya. 2020
0
97.Tendermint blockchain synchronization: formal specification and model checking Braithwaite, Sean and Buchman, Ethan and Konnov, Igor and Milosevic, Zarko and Stoilkovska, Ilina and Widder, Josef and Zamfir, Anca. 2020
0
98.Formal Verification of Ethereum Smart Contracts Using Isabelle/HOL Ribeiro, Maria and Adao, Pedro and Mateus, Paulo. 2020
0
99.Verification of recursive Bitcoin contracts Bartoletti, Massimo and Lande, Stefano and Murgia, Maurizio and Zunino, Roberto. 2020
0
100.Smart Derivatives: On-Chain Forwards for Digital Assets Rius, Alfonso DDM and Gashier, Eamonn. 2020
0
101.Functional Verification of Smart Contracts via Strong Data Integrity Ahrendt, Wolfgang and Bubel, Richard. 2020
0
102.Specifying Framing Conditions for Smart Contracts Beckert, Bernhard and Schiffl, Jonas. 2020
0
103.Efficient Verification of Optimized Code: Correct High-speed Curve25519 Schoolderman, Marc and Moerman, Jonathan and Smetsers, Sjaak and van Eekelen, Marko. 2020
0
104.A tool for proving Michelson Smart Contracts in WHY3 da Horta, Lu\'\is Pedro Arrojado and Reis, Jo\~ao Santos and de Sousa, Sim\~ao Melo and Pereira, M\'ario. 2020
0
105.EthVer: Formal verification of randomized Ethereum smart contracts Mazurek, \Lukasz. 2021
0
106.Formal Modelling and Security Analysis of Bitcoin's Payment Protocol Modesti, Paolo and Shahandashti, Siamak F and McCorry, Patrick and Hao, Feng. 2021
0
107.Efficient Verification of Optimized Code: Correct High-speed X25519 Marc Schoolderman and Jonathan Moerman and Sjaak Smetsers and Marko van Eekelen. 2021
0
108.What is an EUTxO blockchain? Gabbay, Murdoch J. 2020
0
109.Translation Certification for Smart Contracts Krijnen, Jacco and Chakravarty, Manuel MT and Keller, Gabriele and Swierstra, Wouter. 2021
0
110.Sn{\aa}rkl: Somewhat Practical, Pretty Much Declarative Verifiable Computing in Haskell Stewart, Gordon and Merten, Samuel and Leland, Logan. 2018
0
111.Elysium: Automagically Healing Vulnerable Smart Contracts Using Context-Aware Patching Torres, Christof Ferreira and Jonker, Hugo and State, Radu. 2021
0
112.Formalising Decentralised Exchanges in Coq Nielsen, Eske Hoy and Annenkov, Danil and Spitters, Bas. 2022
0
113.ZK-SecreC: a Domain-Specific Language for Zero Knowledge Proofs Bogdanov, Dan and J\"a\"ager, Joosep and Laud, Peeter and Nestra, H\"armel and Pettai, Martin and Randmets, Jaak and Sokk, Ville and Tali, Kert and Valdma, Sandhra-Mirella. 2022
0

Videos

–