formal-methods 
Papers (77)
| # | Title | |
| 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 | |
| 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 | |
| 3. | Defining the ethereum virtual machine for interactive theorem provers Hirai, Yoichi. 2017 | |
| 4. | A Semantic Framework for the Security Analysis of Ethereum smart contracts Grishchenko, Ilya and Maffei, Matteo and Schneidewind, Clara. 2018 | |
| 5. | Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL Amani, Sidney and B\'egel, Myriam and Bortin, Maksym and Staples, Mark. 2018 | |
| 6. | Designing secure Ethereum smart contracts: A finite state machine based approach Mavridou, Anastasia and Laszka, Aron. 2017 | |
| 7. | A concurrent perspective on smart contracts Sergey, Ilya and Hobor, Aquinas. 2017 | |
| 8. | 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 | |
| 9. | Scilla: a Smart Contract Intermediate-Level LAnguage Sergey, Ilya and Kumar, Amrit and Hobor, Aquinas. 2018 | |
| 10. | Validation of decentralised smart contracts through game theory and formal methods Bigi, Giancarlo and Bracciali, Andrea and Meacci, Giovanni and Tuosto, Emilio. 2015 | |
| 11. | Simplicity: A new language for blockchains O'Connor, Russell. 2017 | |
| 12. | Formal verification of smart contracts based on users and blockchain behaviors models Abdellatif, Tesnim and Brousmiche, Kei-L\'eo. 2018 | |
| 13. | Mechanising Blockchain Consensus P\^\irlea, George and Sergey, Ilya. 2018 | |
| 14. | 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 | |
| 15. | A formal verification tool for Ethereum VM Bytecode Park, Daejun and Zhang, Yi and Saxena, Manasvi and Daian, Philip and Ro\csu, Grigore. 2018 | |
| 16. | Modeling bitcoin contracts by timed automata Andrychowicz, Marcin and Dziembowski, Stefan and Malinowski, Daniel and Mazurek, \Lukasz. 2014 | |
| 17. | VerX: Safety Verification of Smart Contracts Permenev, Anton and Dimitrov, Dimitar and Tsankov, Petar and Drachsler-Cohen, Dana and Vechev, Martin. 2019 | |
| 18. | Exploiting the laws of order in smart contracts Kolluri, Aashish and Nikolic, Ivica and Sergey, Ilya and Hobor, Aquinas and Saxena, Prateek. 2019 | |
| 19. | Towards safer smart contracts: A survey of languages and verification methods Harz, Dominik and Knottenbelt, William. 2018 | |
| 20. | Raziel: private and verifiable smart contracts on blockchains S\'anchez, David Cerezo. 2018 | |
| 21. | Model-Checking of Smart Contracts Nehai, Zeinab and Piriou, Pierre-Yves and Daumas, Frederic. 2018 | |
| 22. | Smt-based verification of solidity smart contracts Alt, Leonardo and Reitwiessner, Christian. 2018 | |
| 23. | VeriSolid: Correct-by-Design Smart Contracts for Ethereum Mavridou, Anastasia and Laszka, Aron and Stachtiari, Emmanouela and Dubey, Abhishek. 2019 | |
| 24. | Formal verification of Deed contract in Ethereum name service Hirai, Yoichi. 2016 | |
| 25. | Marlowe: Financial contracts on blockchain Seijas, Pablo Lamela and Thompson, Simon. 2018 | |
| 26. | 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 | |
| 27. | solc-verify: A Modular Verifier for Solidity Smart Contracts Hajdu, \'Akos and Jovanovi\'c, Dejan. 2019 | |
| 28. | Smart contracts and opportunities for formal methods Miller, Andrew and Cai, Zhicheng and Jha, Somesh. 2018 | |
| 29. | Monitoring smart contracts: Contractlarva and open challenges beyond Azzopardi, Shaun and Ellul, Joshua and Pace, Gordon J. 2018 | |
| 30. | Temporal Properties of Smart Contracts Sergey, Ilya and Kumar, Amrit and Hobor, Aquinas. 2018 | |
| 31. | Automated Verification of Electrum Wallet Mathieu Turuani and Thomas Voegtlin and Micha\"el Rusinowitch. 2016 | |
| 32. | 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 | |
| 33. | Developing secure Bitcoin contracts with BitML Atzei, Nicola and Bartoletti, Massimo and Lande, Stefano and Yoshida, Nobuko and Zunino, Roberto. 2019 | |
| 34. | On the specification and verification of atomic swap smart contracts⋆ van der Meyden, Ron. 2018 | |
| 35. | Smart Contract Interactions in Coq Nielsen, Jakob Botsch and Spitters, Bas. 2019 | |
| 36. | Formal Specification and Verification of Smart Contracts for Azure Blockchain Lahiri, Shuvendu K and Chen, Shuo and Wang, Yuepeng and Dillig, Isil. 2018 | |
| 37. | 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 | |
| 38. | Executable Operational Semantics of Solidity Jiao, Jiao and Kan, Shuanglong and Lin, Shang-Wei and Sanan, David and Liu, Yang and Sun, Jun. 2018 | |
| 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 | |
| 40. | 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 | |
| 41. | A minimal core calculus for Solidity contracts Bartoletti, Massimo and Galletta, Letterio and Murgia, Maurizio. 2019 | |
| 42. | 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 | |
| 43. | 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 | |
| 44. | Proof-Carrying Smart Contracts Dickerson, Thomas and Gazzillo, Paul and Herlihy, Maurice and Saraph, Vikram and Koskinen, Eric. 2018 | |
| 45. | 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 | |
| 46. | Albert, an intermediate smart-contract language for the Tezos blockchain Bernardo, Bruno and Cauderlier, Rapha\"el and Pesin, Basile and Tesson, Julien. 2020 | |
| 47. | Cross-Chain Payment Protocols with Success Guarantees van Glabbeek, Rob and Gramoli, Vincent and Tholoniat, Pierre. 2019 | |
| 48. | ConCert: A Smart Contract Certification Framework in Coq Annenkov, Danil and Nielsen, Jakob Botsch and Spitters, Bas. 2020 | |
| 49. | 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 | |
| 50. | Formalising and verifying smart contracts with Solidifier: a bounded model checker for Solidity Antonino, Pedro and Roscoe, AW. 2020 | |
| 51. | 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 | |
| 52. | Toychain: Formally Verified Blockchain Consensus George P\^ırlea. 2019 | |
| 53. | Contingent payments on a public ledger: models and reductions for automated verification. Bursuc, Sergiu and Kremer, Steve. 2019 | |
| 54. | 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 | |
| 55. | Renegotiation and recursion in Bitcoin contracts Bartoletti, Massimo and Murgia, Maurizio and Zunino, Roberto. 2020 | |
| 56. | Domain Specific Language for Smart Contract Development W\"ohrer, Maximilian and Zdun, Uwe. 2020 | |
| 57. | Termination of Ethereum's Smart Contracts Genet, Thomas and Jensen, Thomas and Sauvage, Justine. 2020 | |
| 58. | 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 | |
| 59. | eThor: Practical and Provably Sound Static Analysis of Ethereum Smart Contracts Schneidewind, Clara and Grishchenko, Ilya and Scherer, Markus and Maffei, Matteo. 2020 | |
| 60. | Formal Specification and Verification of Solidity Contracts with Events Hajdu, Akos and Jovanovic, Dejan and Ciocarlie, Gabriela. 2020 | |
| 61. | 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 | |
| 62. | 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 | |
| 63. | Smart Contract modeling and verification techniques: A survey Imeri, Adnan and Agoulmine, Nazim and Khadraoui, Djamel. 2020 | |
| 64. | 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 | |
| 65. | 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 | |
| 66. | 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 | |
| 67. | 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 | |
| 68. | Formal specification of a security framework for smart contracts Mandrykin, Mikhail and O'Shannessy, Jake and Payne, Jacob and Shchepetkov, Ilya. 2020 | |
| 69. | Towards declarative smart contracts Purnell, Kevin and Schwitter, Rolf. 2019 | |
| 70. | Accountability in a Permissioned Blockchain: Formal Analysis of Hyperledger Fabric Ralf Kuesters and Daniel Rausch and Mike Simon. 2020 | |
| 71. | 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 | |
| 72. | Flexible Formality Practical Experience with Agile Formal Methods Szamotulski, Marcin and Vinogradova, Polina. 2020 | |
| 73. | SmartBugs: A Framework to Analyze Solidity Smart Contracts Ferreira, Jo\~ao F and Cruz, Pedro and Durieux, Thomas and Abreu, Rui. 2020 | |
| 74. | Model Checking Bitcoin and other Proof-of-Work Consensus Protocols DiGiacomo-Castillo, Max and Liang, Yiyun and Pal, Advay and Mitchell, John C. 2020 | |
| 75. | Formalizing Nakamoto-Style Proof of Stake Søren Eller Thomsen and Bas Spitters. 2020 | |
| 76. | 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 | |
| 77. | 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 |
Videos
–