The dataset serves as the supplementary material for a survey of formal specification and verification of smart contracts.
| Publication | Authors | Venue | Year | Keywords | Platform |
|---|---|---|---|---|---|
| A model-driven approach to smart contract development | Boogaard | Master's Thesis | 2018 | Program synthesis, Validation, ADICO statements, FSM | Ethereum |
| Secure smart contract generation based on Petri Nets | Zupan et al. | Blockchain Technology for Industry 4.0 | 2020 | Petri Nets, Validation, Program synthesis | Ethereum, Hyperledger Fabric is future work |
| Building executable secure design models for smart contracts with formal methods | Xu and Fink | WTSC@FC | 2019 | Set-based methods, TLA+, Design patterns, Legal contract | Ethereum |
| Automatic smart contract generation using controlled natural language and template | Tateishi et al. | IBM Journal of Research and Development | 2019 | Program synthesis, LDLf, ECA rules, Template, SCXML, Statechart, DSL4SC | Hyperledger Fabric |
| Tool demonstration: FSolidM for designing secure Ethereum smart contracts | Mavridou and Laszka | POST | 2018 | Program synthesis, FSM, Design patterns, FSolidM | Ethereum |
| Specification mining for smart contracts with automatic abstraction tuning execution trace | Guth et al. | arXiv | 2018 | Execution trace, Event abstraction, Dependency graph, Specification mining | Ethereum |
| Towards model-driven engineering of smart contracts for cyber-physical systems | Garamvölgyi et al. | IEEE DNS Workshops | 2018 | Program synthesis, YAKINDU, Cyber-physical system, Access control | Ethereum |
| Smart contract design meets state machine synthesis: Case studies | Suvorov and Ulyantsev | arXiv | 2019 | LTL, Program synthesis, EFSM-tools | Ethereum |
| Caterpillar: A business process execution engine on the Ethereum blockchain | López-Pintado et al. | Software: Practice and Experience | 2019 | Program synthesis, Monitoring, BPMN | Ethereum |
| Optimized execution of business processes on blockchain | Garcı́a-Bañuelos et al. | BPM | 2017 | Program synthesis, BPMN, Petri nets | Ethereum |
| Untrusted business processes monitoring and execution using blockchain | Weber et al. | BPM | 2016 | Program synthesis, Monitoring, BPMN | Ethereum |
| Who Spent My EOS? On the (In)Security of Resource Management of EOS.IO | Lee et al. | USENIX WOOT | 2019 | Resource consumption, Exploit generation | EOS.IO |
| SmartInspect: Solidity smart contract inspector | Bragagnolo | IEEE IWBOSE@SANER | 2018 | Inspection, AST | Ethereum |
| Is solidity solid enough? | Crafa et al. | WTSC@FC | 2019 | Formal semantics, Solidity, Featherweight Solidity | Ethereum |
| Beagle: A new framework for smart contracts taking account of law | Tsai et al. | IEEE SOSE | 2019 | DSL, Legal contract | N/A |
| Gigahorse: thorough, declarative decompilation of smart contracts | Grech et al. | IEEE/ACM ICSE | 2019 | CFG, Decompilation, Datalog | Ethereum |
| How effective are smart contract analysis tools? Evaluating smart contract static analysis tools using bug injection | Ghaleb and Pattabiraman | ACM ISSTA | 2020 | Bug injection, Evaluation | Ethereum |
| SIF: A framework for Solidity contract instrumentation and analysis | Peng et al. | IEEE APSEC | 2019 | Bug injection, Code instrumentation, Program synthesis, AST | Ethereum |
| Lorikeet: A model-driven engineering tool | Tran et al. | BPM | 2018 | BPMN, Model-driven engineering, Program synthesis | Ethereum |
| The treewidth of smart contracts | Chatterjee et al. | ACM SAC | 2019 | CFG, Treewidth | Ethereum |
| Proof-carrying smart contract | Dickerson et al. | WTSC@FC | 2018 | Proof-carrying code, Hoare-style properties, In theory: Why3, Boogie verification | Ethereum |
| From institutions to code: Towards automated generation of smart contracts | Frantz and Nowostawski | IEEE FAS*W | 2016 | Program synthesis, DSL, ADICO statements | Ethereum |
| SoK: unraveling Bitcoin smart contracts | Atzei et al. | POST | 2018 | DSL, Process algebra, Formal semantics | Bitcoin |
| Porthos: macroprogramming blockchain systems | Mizzi et al. | IFIP NTMS | 2019 | DSL, Commitment, Inter-chain communication, Peyton Jones | Hyperledger Fabric, Ethereum |
| Marlowe: Financial Contracts on Blockchain | Lamela Seijas and Thompson | ISoLA | 2018 | DSL, Marlowe Language, Formal semantics, Haskell, Peyton Jones | Cardano |
| Fun with Bitcoin Smart Contracts | Bartoletti et al. | ISoLA | 2018 | DSL, Process algebra, BitML | Bitcoin |
| Writing Safe Smart Contracts in Flint | Schrans et al. | ACM Programming | 2018 | Programming language, Asset (Linear) type, Writing restrictions | Ethereum |
| Domain specific language for smart contract development | Wohrer and Zdun | IEEE ICBC | 2020 | DSL, Program synthesis, CML | Ethereum |
| SmaCoNat: Smart contracts in natural language | Regnath and Steinhorst | FDL | 2018 | DSL, Cyber-physical system | N/A |
| Designing secure Ethereum smart contracts: A finite state machine based approach | Mavridou and Laszka | WTSC@FC | 2018 | Program synthesis, FSM, Design patterns, FSolidM | Ethereum |
| Findel: Secure derivative contracts for Ethereum | Biryukov et al. | WTSC@FC | 2017 | DSL, Financial derivative, Peyton Jones | Ethereum |
| A minimal core calculus for Solidity contracts | Bartoletti et al. | ESORICS, DPM and CBT | 2019 | Formal semantics, Solidity, TinySol | Ethereum |
| SPESC: A specification language for smart contracts | He et al. | IEEE COMPSAC | 2018 | DSL, Legal contract | Ethereum |
| BitML: A calculus for Bitcoin smart contracts | Bartoletti and Zunino | ACM CCS | 2018 | DSL, Process algebra, Formal semantics, BitML | Bitcoin |
| Flint for safer smart contracts | Schrans et al. | arXiv | 2019 | Programming language, Asset (Linear) type, Writing restrictions | Ethereum |
| Certifying Findel derivatives for blockchain | Arusoaie | arXiv | 2020 | DSL, Thorem proving, Formal semantics, Coq, Peyton Jones, Financial derivatives | Ethereum |
| Defining the Ethereum virtual machine for interactive theorem provers | Hirai | WTSC@FC | 2017 | Theorem proving, Isabelle/HOL, Formal semantics, Vulnerabilities, EVM, Deed | Ethereum |
| Marlowe: implementing and analysing financial contracts on blockchain | Lamela Seijas et al. | WTSC@FC | 2020 | DSL, Theorem proving, Isabelle/HOL, Static analysis, Haskell SBV, Peyton Jones, Language meta-theory | Cardano |
| Termination of Ethereum's smart contracts | Genet et al. | Research Report | 2020 | Theorem proving, Isabelle/HOL, Formal semantics, EVM, Resource consumption | Ethereum |
| Formal verification of Deed contract in Ethereum Name Service | Hirai | Personal Website | 2016 | Theorem proving, Isabelle/HOL, Lem, EVM, Access Control, Deed | Ethereum |
| Towards verifying Ethereum smart contracts at intermediate language level | Li et al. | ICFEM | 2019 | Theorem proving, Isabelle/HOL, Yul, Functional correctness, Safe arithmetics | Ethereum |
| Formal specification of a security framework for smart contracts | Mandrykin et al. | FMBC@FM | 2019 | Theorem proving, Isabelle/HOL, Cap9 | Ethereum |
| Towards verifying ethereum smart contract bytecode in Isabelle/HOL | Amani et al. | ACM CPP | 2018 | Theorem proving, Isabelle/HOL, Hoare logic, Program logic | Ethereum |
| A hybrid formal verification system in Coq for ensuring the reliability and security of Ethereum-based service smart contracts | Yang et al. | IEEE Access | 2020 | Theorem proving, Coq, Static analysis, Symbolic & concolic execution, Hoare logic, Memory model, FEther, Lolisa, FSPVM-E | Ethereum |
| FEther: An extensible definitional interpreter for smart-contract verifications in Coq | Yang and Lei | IEEE Access | 2020 | Theorem proving, Coq, Symbolic & concolic execution, Formal semantics | Ethereum |
| Lolisa: Formal syntax and semantics for a subset of the Solidity programming language | Yang and Lei | arXiv | 2018 | Theorem proving, Coq, Formal semantics, Language meta-theory, Solidity | Ethereum |
| Albert, an intermediate smart-contract language for the Tezos blockchain | Bernardo et al. | WTSC@FC | 2019 | Certified compilation, Coq, Ott framework, Linear types | Tezos |
| Towards verification of Ethereum smart contracts: A formalization of core of Solidity | Zakrzewski | VSTTE@CAV | 2018 | Theorem proving, Coq, Formal semantics, Solidity | Ethereum |
| Simplicity: A new language for blockchains | O'Connor | ACM PLAS@PLDI | 2017 | Programming language, Theorem proving, Coq, Formal semantics, Language meta-theory | Bitcoin and Bitcoin-like |
| Pluralize: a trustworthy framework for high-level smart contract-draft | Dargaye et al. | arXiv | 2018 | Trust management, Theorem proving, Coq, DSL | Blockchain ADT |
| Towards secure and trusted-by-design smart contracts | Dargaye et al. | JFLA | 2018 | Theorem proving, Coq, Trust management | Blockchain ADT |
| Temporal properties of smart contracts | Sergey et al. | ISoLA | 2018 | Theorem proving, Coq, Formal trace semantics, Scilla | Ethereum, Zilliqa |
| Mi-Cho-Coq, a framework for certifying Tezos Smart Contracts | Bernardo et al. | FMBC@FM | 2019 | Theorem proving, Coq, Weakest precondition calculus, Functional correctness, Michelson | Tezos |
| Towards a smart contract verification framework in Coq | Annenkov and Spitters | FMBC@FM | 2019 | Theorem proving, Coq, Language meta-theory, Oak, AST, MetaCoq, Functional correctness | N/A |
| Smart contract interactions in Coq | Nielsen and Spitters | FMBC@FM | 2019 | Theorem proving, Coq, Inter-contract analysis, Shallow embedding, Invariant, Congress | Depth-first (Ethereum) and breadth-first (Tezos) execution blockchains |
| A formal verification framework for security issues of blockchain smart contracts | Sun and Yu | Electronics | 2020 | Theorem proving, Coq, Integer overflow, Functional correctness, Invariants, Access control, BNB | Ethereum |
| ConCert: A smart contract certification framework in Coq | Annenkov et al. | ACM CPP | 2020 | Theorem proving, Coq, MetaCoq, AST, Language meta-theory, Acorn, Functional correctness | N/A |
| Scilla: A Smart Contract Intermediate-Level LAnguage | Sergey et al. | arXiv | 2018 | Theorem proving, Coq | Zilliqa |
| Raziel: Private and verifiable smart contracts on blockchains | Sanchez | arXiv | 2020 | Proof-carrying code, Theorem proving, Coq, Privacy, NIZK proof, Obliv-Java, JML | OmniLedger, Hyperledger Fabric, Ethereum |
| System F in Agda, for fun and profit | Chapman et al. | MPC | 2019 | Formal Semantics, Language meta-theory, Agda, Plutus Core | Cardano |
| Blockchains as Kripke models: An analysis of atomic cross-chain swap | Hirai | ISoLA | 2018 | Intuitionistic epistemic logic, Kripke model, Hashlock, Atomicity, Atomic swap | N/A (Cross-chain) |
| Obsidian: Typestate and assets for safer blockchain programming | Coblenz et al. | arXiv | 2019 | Programming language, State-oriented programming, Linear types, Language meta-theory | Hyperledger Fabric |
| Resources: A safe language abstraction for Mmney | Blackshear et al. | arXiv | 2020 | Move, Linear types, Language meta-theory | Libra |
| Exploiting the laws of order in smart contracts | Kolluri et al. | ACM ISSTA | 2019 | Symbolic execution, Z3, Fuzzing, Event-ordering vulnerabilities, EthRacer | Ethereum |
| VerX: Safety verification of smart contracts | Permenev et al. | IEEE S&P | 2020 | Symbolic execution, Z3, Delayed predicate abstraction, Reachability checking, ptLTL | Ethereum |
| Security analysis of EOSIO smart contracts | He et al. | arXiv | 2020 | Symbolic execution, Z3, Static analysis, Vulnerabilities, EOSafe | EOS.IO |
| Security assurance for smart contract | Zhou et al. | IFIP NTMS | 2018 | Symbolic execution, Z3, Syntax analysis, Topological analysis, Oyente, SASC | Ethereum |
| The art of the scam: Demystifying honeypots in Ethereum smart contracts | Ferreira Torres et al. | USENIX Security | 2019 | Symbolic execution, Z3, Heuristics, Oyente, HoneyBadger | Ethereum |
| Under-optimized smart contracts devour your money | Chen et al. | IEEE SANER | 2017 | Symbolic execution, Z3, Resource consumption, CFG, Inefficient patterns, Gasper | Ethereum |
| sCompile: Critical path identification and analysis for smart contracts | Chang et al. | ICFEM | 2019 | Symbolic execution, Z3, CFG, Monetary paths | Ethereum |
| Smashing Ethereum smart contracts for fun and real profit | Mueller | HITB SecConf | 2018 | Symbolic execution, Z3, CFG, Vulnerabilities, Mythril | Ethereum |
| Manticore: A User-Friendly Symbolic Execution Framework for Binaries and smart contracts | Mossberg et al. | IEEE/ACM ASE | 2019 | Symbolic execution, Z3, CFG, Vulnerabilities | Ethereum |
| Finding the greedy, prodigal, and suicidal contracts at scale | Nikolić et al. | ACSAC | 2018 | Symbolic execution, Z3, Trace properties, Exploit generation, Maian | Ethereum |
| teEther: Gnawing at ethereum to automatically exploit smart contracts | Krupp and Rossow | USENIX Security | 2018 | Symbolic execution, Z3, Exploit generation, CFG, Trace properties, Vulnerabilities | Ethereum |
| Osiris: Hunting for integer bugs in Ethereum smart contracts | Ferreira Torres et al. | ACM ACSAC | 2018 | Symbolic execution, Z3, Oyente, Integer bugs | Ethereum |
| Detecting standard violation errors in smart contracts | Li and Long | arXiv | 2019 | Symbolic execution, Boolector, Invariants, ERC20, ERC721 | Ethereum |
| Making smart contracts smarter | Luu et al. | ACM CCS | 2016 | Symbolic execution, Z3, CFG, Oyente | Ethereum |
| Evaluating spread of 'Gasless Send' in Ethereum smart contracts | Prechtel et al. | IFIP NTMS | 2019 | Symbolic Execution Z3, Resource consumption, Mythril | Ethereum |
| Precise attack synthesis for smart contracts | Feng et al. | arXiv | 2019 | Symbolic execution, Boolector, Abstract interpretation, Exploit generation, Racket, Vulnerabilities | Ethereum |
| Annotary: A concolic execution system for developing secure smart contracts | Weiss and Schütte | ESORICS | 2019 | Concolic execution, Invariants, Writing restrictions, Inter-contract analysis, Mythril | Ethereum |
| Towards automated verification of smart contract fairness | Liu et al. | ACM ESEC/FSE | 2020 | Symbolic execution, Z3, Dafny, Mechanism design, Invariants, FairCon | Ethereum |
| On the Prediction of smart contracts' Behaviours | Laneve et al. | From Software Engineering to Formal Methods and Tools, and Back | 2019 | Symbolic analysis, Process algebra, scl, Objective function, Game theory | Ethereum |
| SmartCheck: Static analysis of Ethereum smart contracts | Tikhomitov et al. | IEEE/ACM WETSEB@ICSE | 2018 | Syntactic analysis, Pattern matching, XML, XPath, Vulnerabilities | Ethereum |
| SolidityCheck: Quickly detecting smart contract problems through regular expressions | Zhang et al. | arXiv | 2019 | Syntactic analysis, Pattern matching, RegEx | Ethereum |
| NeuCheck: A more practical Ethereum smart contract security analysis tool | Lu et al. | Software: Practice and experience | 2019 | Syntactic analysis, Pattern matching, XML, XPath, Vulnerabilities | Ethereum |
| Potential risks of Hyperledger Fabric smart contracts | Yamashita et al. | IEEE IWBOSE@SANER | 2019 | Syntactic analysis, AST, Vulnerabilities | Hyperledger Fabric |
| ReJection: A AST-based reentrancy vulnerability detection method | Ma et al. | CTCIS | 2020 | Syntactic analysis, AST, Reentrancy, Slither | Ethereum |
| Why do smart contracts self-destruct? Investigating the Selfdestruct function on Ethereum | Chen et al. | arXiv | 2020 | Syntactic analysis, AST, Execution trace, Machine learning, Access control | Ethereum |
| EthPloit: From fuzzing to efficient exploit generation against smart contracts | Zhang et al. | IEEE SANER | 2020 | Fuzzing, Taint analysis, Exploit generation | Ethereum |
| Towards Smart Hybrid Fuzzing for smart contracts | Ferreira Torres et al. | arXiv | 2020 | Fuzzing, Symbolic execution | Ethereum |
| Learning to fuzz from symbolic execution with application to smart contracts | He et al. | ACM CCS | 2019 | Fuzzing, Symbolic execution, Imitation-based learning | Ethereum |
| VULTRON: Catching vulnerable smart contracts once and for all | Wang et al. | IEEE/ACM ICSE | 2019 | Fuzzing, Test oracles, Invariants | Ethereum |
| ContractFuzzer: Fuzzing smart contracts for vulnerability detection | Jiang et al. | IEEE/ACM ASE | 2018 | Fuzzing, Test oracles, Vulnerabilities, Instrumented EVM | Ethereum |
| Harvey: A greybox fuzzer for smart contracts | Wustholz and Christakis | arXiv | 2019 | Demand-driven sequence fuzzing, Input prediction, Vulnerabilities | Ethereum |
| Oracle-supported dynamic exploit generation for smart contracts | Wang et al. | arXiv | 2019 | Fuzzing, Test oracles, Invariants, Exploit Generation | Ethereum |
| ReGuard: Finding reentrancy bugs in smart contracts | Liu et al. | IEEE/ACM ICSE | 2018 | Fuzzing, C++, Automata, Reentrancy, Execution trace | Ethereum |
| Contracts over smart contracts: Recovering from violations dynamically | Colombo et al. | ISoLA | 2018 | Runtime verification, Checkpoining, Recovery, Code update, ContractLarva | Ethereum |
| Monitoring smart contracts: Contractlarva and open challenges beyond | Pace et al. | RV | 2018 | Runtime verification, Contract instrumentation, Contractlarva, ERC20, Procurement | Ethereum |
| Runtime verification of Ethereum smart contracts | Pace and Ellul | IEEE EDCC | 2018 | Runtime verification, Contract instrumentation, Contractlarva, Casino | Ethereum |
| TokenScope: Automatically detecting inconsistent behaviors of cryptocurrency tokens in Ethereum | Chen et al. | ACM CCS | 2019 | Runtime verification, Execution trace, ERC20 | Ethereum |
| EthScope: A transaction-centric security analytics framework to detect malicious smart contracts on Ethereum | Wu et al. | arXiv | 2020 | Runtime verification, Code instrumentation, EVM instrumentation, Execution trace | Ethereum |
| EVM*: From offline detection to online reinforcement for Ethereum Virtual Machine | Ma et al. | IEEE SANER | 2019 | Runtime verification, EVM instrumentation, js-evm, Integer overflow, Timestamp dependency | Ethereum |
| Sereum: Protecting existing smart contracts against re-entrancy attacks | Rodler et al. | NDSS | 2019 | Runtime verification, Taint analysis, EVM instrumentation, Reentrancy | Ethereum |
| Online detection of Effectively Callback Free objects with applications to smart contracts | Grossman et al. | ACM POPL | 2018 | Runtime verification, Static analysis, Serializability, Execution trace, EVM instrumentation, Reentrancy | Ethereum |
| Implementation of smart contracts using hybrid architectures with on- and off-blockchain components | Molina-Jimenez et al. | IEEE SC2 | 2018 | Runtime verification, Contract Compliance Checker, Model checking, SPIN, Legal contract | Ethereum |
| Enriching smart contracts with temporal aspects | Fournier and Skarbovsky | ICBC | 2019 | Runtime verification, Complex event processing, CEP PROTON, Supply chain | Hyperledger Fabric, Composer |
| Solitor: Runtime verification of smart contracts on the Ethereum network | Stegeman | Master's Thesis | 2018 | Runtime verification, Annotations, Code instrumentation, DSL, ANTLR, Solidity | Ethereum |
| On observing contracts: deontic contracts meet smart contracts | Azzopardi et al. | JURIX | 2018 | Runtime verification, Code instrumentation, Deontic logic, Formal semantics, Legal contract | Ethereum |
| SolAnalyser: A framework for analysing and testing smart contracts | Akca et al. | IEEE APSEC | 2019 | Runtime verification, Testing, Code instrumentation, Bug injection, AST | Ethereum |
| SODA: A generic online detection framework for smart contracts | Chen et al. | NDSS | 2020 | Runtime verification, Client instrumentation, ERC20 | Ethereum |
| EASYFLOW: Keep Ethereum away from overflow | Gao et al. | IEEE/ACM ICSE Companion | 2019 | Runtime verification, EVM instrumentation, Pattern matching, Integer overflow | Ethereum |
| Ethereum smart contracts verification: A survey and a prototype tool | Bogdanich Espina | Bachelor's Thesis | 2019 | Runtime verification, ptLTL, Code instrumentation, Slither, VeriSol, Manticore | Ethereum |
| Securing smart contract with runtime validation | Li et al. | ACM PLDI | 2020 | Runtime verification, Code instrumentation, Invariants, ERC20, ERC721, ERC1202 | Ethereum |
| Ægis: Smart shielding of smart contracts | Ferreira Torres et al. | ACM CCS | 2019 | Runtime verification, Instrumented EVM, DSL, Patterns | Ethereum |
| Securing smart contracts on the fly | Li et al. | arXiv | 2019 | Runtime verification, Code instrumentation, Invariants, ERC20, ERC721, ERC1202 | Ethereum |
| A federated society of bots for smart contract testing | Viglianisi et al. | Journal of Systems and Software | 2020 | Testing, Static analysis, Z3, Invariants, EIP20, SoCRATES | Ethereum |
| Reentrancy vulnerability identification in Ethereum smart contracts | Samreen and Alalfi | IEEE IWBOSE@SANER | 2020 | Testing, Syntactic analysis, AST | Ethereum |
| EtherTrust: Sound static analysis of Ethereum bytecode | Grishchenko et al. | Technical Report | 2018 | Program verification, Reachability analysis, Horn clauses | Ethereum |
| eThor: Practical and provably sound static analysis of Ethereum smart contracts | Schneidewind et al. | ACM CCS | 2020 | Program verification, Reachability analysis, Horn clauses, Hoare logic, HoRSt, DSL, Single-entrancy | Ethereum |
| Foundations and tools for the static analysis of Ethereum smart contracts | Grishchenko et al. | CAV | 2018 | Program verification, Reachability analysis | Ethereum |
| Deductive proof of Ethereum smart contracts using Why3 | Nehaı̈ and Bobot | FMBC@FM | 2019 | Deductive verification, Why3, Why3 FOL, Runtime errors, Functional correctness, Marketplace | Ethereum |
| Towards a formally verified EVM in production environment | Zhang et al. | COORDINATION | 2020 | Deductive verification, Why3, Why3 FOL, Functional correctness, Integer overflow, Auction | Ethereum |
| WhylSon: Proving your Michelson smart contracts in Why3 | Horta et al. | FMBC@CAV | 2020 | Deductive verification, Why3, Why3 FOL, Multisig, Factorial | Tezos |
| GASOL: Gas analysis and optimization for Ethereum smart contracts | Albert et al. | TACAS | 2020 | Resource consumption, Resource optimization, Static analysis | Ethereum |
| Formal verification of Solidity contracts in Event-B | Zhu et al. | arXiv | 2020 | Set-based methods, Event-B, Rodin, Honeypot | Ethereum |
| Evaluation of logic-based smart contracts for blockchain systems | Idelberger et al. | RuleML | 2016 | Deontic defeasible logic, FCL, SPINdle | N/A |
| On legal contracts, imperative and declarative smart contracts, and blockchain systems | Governatori et al. | Artificial Intelligence and Law | 2018 | Deontic defeasible logic, FCL, SPINdle | N/A |
| ZEUS: Analyzing safety of smart contracts | Kalra et al. | NDSS | 2018 | LLVM, Model checking, Seahorn, Constrained Horn clauses, Abstract interpretation, Code instrumentation, XACML, FOL | Ethereum, Hyperledger Fabric |
| Detecting nondeterministic payment bugs in Ethereum smart contracts | Wang et al. | ACM OOPSLA | 2019 | LLVM, Bounded model checking, SMACK, Taint analysis | Ethereum |
| Smart contracts: Application scenarios for deductive program verification | Beckert et al. | FMBC@FM | 2019 | Deductive verification, KeY, JML, JavaDL, Program logic | Hyperledger Fabric |
| Formal specification and verification of Hyperledger Fabric chaincode | Beckert et al. | SDLT@ICFEM | 2018 | Deductive verification, KeY, JML, JavaDL, Program logic | Hyperledger Fabric |
| Smart contracts: A killer application for deductive source code verification | Ahrendt et al. | Principled Software Development | 2018 | Deductive verification, KeY, JML, JavaDL, Program logic | Ethereum |
| Verification of smart contract business logic | Ahrendt et al. | FSEN | 2019 | Deductive verification, KeY, JML, JavaDL, Program logic, Solidity | Ethereum |
| Semantic understanding of smart contracts: Executable operational semantics of Solidity | Jiao et al. | IEEE S&P | 2020 | K framework, Formal semantics, Solidity | Ethereum |
| A language-independent approach to smart contract verification | Chen et al. | ISoLA | 2018 | K framework, Reachability logic, EVM, ERC20 | Ethereum |
| KEVM: A complete formal semantics of the Ethereum Virtual Machine | Hildenbrandt et al. | IEEE CSF | 2018 | K framework, Formal semantics, Reachability logic, Matching logic, EVM | Ethereum |
| IELE: A rigorously designed language and tool ecosystem for the Blockchain | Kasampalis et al. | FM | 2019 | K framework, Formal semantics, Reachability logic, Matching logic, IELE | Ethereum, Any Ethereum-style blockchain |
| A formal verification tool for Ethereum VM bytecode | Park et al. | ACM ESEC/FSE | 2018 | K framework, Formal semantics, Reachability logic, Matching logic, EVM, ERC20 | Ethereum |
| Securing smart contracts with information flow | Cecchetti et al. | FAB | 2020 | Information flow, Integrity, Composite vulnerabilities, Reentrancy | Ethereum |
| Formal verification of smart contracts: Short paper | Bhargavan et al. | ACM PLAS@PLDI | 2016 | F*, Formal semantics, Typechecking, Effects, Resource consumption, Vulnerabilities, Solidity, EVM | Ethereum |
| A semantic framework for the security analysis of ethereum smart contracts | Grishchenko et al. | POST | 2018 | F*, Formal semantics, EVM, Hyper- and safety properties | Ethereum |
| Ethainter: A smart contract security analyzer for composite vulnerabilities | Brent et al. | ACM PLDI | 2020 | Datalog, Soufflé, Information flow, Gigahorse, Composite vulnerabilities, EVM | Ethereum |
| Vandal: A security analysis scalable framework | Brent et al. | arXiv | 2018 | Datalog, Soufflé, CFG, Vulnerable patterns | Ethereum |
| MadMax: Surviving out-of-gas conditions in Ethereum smart contracts | Grech et al. | ACM OOPSLA | 2018 | Datalog, Soufflé, Resource consumption, Vulnerable patterns | Ethereum |
| Securify: Practical security analysis of smart contracts | Tsankov et al. | ACM CCS | 2018 | Datalog, Soufflé, Vulnerable patterns, Compliance patterns, DSL | Ethereum |
| Smart contract vulnerabilities: Does anyone care? | Perez and Livshits | arXiv | 2019 | Datalog, Execution trace, Vulnerable patterns | Ethereum |
| SAFEVM: A safety verifier for Ethereum smart contracts | Albert et al. | ACM ISSTA | 2019 | Static analysis, C, CPAchecker, SeaHorn, VeryMax, Assertions, Array access, EthIR, Oyente | Ethereum |
| solc-verify: A modular verifier for Solidity smart contracts | Hajdu and Jovanović | VSTTE@CAV | 2019 | Boogie, SMT solving, Z3, CVC4, Yices2, Annotations, Invariants, DSL | Ethereum |
| Formal specification and verification of Solidity contracts with events | Hajdu et al. | FMBC@CAV | 2020 | Boogie, SMT solving, Z3, CVC4, Yices2, Annotations, Invariants, DSL | Ethereum |
| Formalising and verifying smart contracts with Solidifier: a bounded model checker for Solidity | Antonino and Roscoe | arXiv | 2020 | Boogie, Bounded model checking, Corral, Memory model, Annotations | Ethereum |
| Formal specification and verification of smart contracts for Azure blockchain | Wang et al. | arXiv | 2019 | Boogie, Bounded model checking, Corral, Code instrumentation, Monomial predicate abstraction | Ethereum, Azure |
| Running on fumes--Preventing out-of-gas vulnerabilities in Ethereum smart contracts using static resource analysis | Albert et al. | VECoS@FM | 2019 | Resource consumption, Static analysis, Oyente, EthIR, SACO, PUBS | Ethereum |
| WIP: Finding bugs automatically in smart contracts with parameterized specifications | Bernardi et al. | Stanford Blockchain Conference | 2020 | Static analysis, Hoare logic, Invariants, Certora prover | Ethereum |
| SMARTSHIELD: Automatic smart contract protection made easy | Zhang et al. | IEEE SANER | 2020 | Static analysis, Repair, Code update, EVM bytecode | Ethereum |
| A method of logic-based smart contracts for blockchain system | Hu and Zhong | ACM ICDPA | 2018 | Active-U-Datalog, On-chain rule engine, License agreement | N/A |
| EVulHunter: Detecting fake transfer vulnerabilities for EOSIO's smart contracts at Webassembly-level | Quan et al. | arXiv | 2019 | Static analysis, CFG, Pattern matching, Vulnerabilities | EOS.IO |
| Proving conditional termination for smart contracts | Le et al. | ACM BCC@Asia CCS | 2018 | Static analysis, Conditional termination, Runtime enforcement | Ethereum |
| Tezla, an intermediate representation for static analysis of Michelson smart contracts | Reis et al. | FMBC@CAV | 2020 | Static analysis, SoftCheck | Tezos |
| EthBMC: A bounded model checker for smart contracts | Frank et al. | USENIX Security | 2020 | Bounded model checking, Symbolic execution, Yices2, Boolector, Z3, Memory model, Inter-contract analysis | Ethereum |
| Safer smart contract programming with Scilla | Sergey et al. | ACM OOPSLA | 2019 | Programming language, System F, CPS, Communicating automata, Static analysis, Resource consumption, Cashflow analysis | Zilliqa |
| Slither: A static analysis framework for smart contracts | Feist et al. | IEEE/ACM WETSEB@ICSE | 2019 | Static analysis, Intermediate representation, Code summarization, Vulnerable patterns, SlithIR | Ethereum |
| EthIR: A framework for high-level analysis of Ethereum bytecode | Albert et al. | ATVA | 2018 | Static analysis, Intermediate representation, Oyente | Ethereum |
| SMT-based verification of Solidity smart contracts | Alt and C. Reitwiessner | ISoLA | 2018 | Bounded model checking, SMT solving, Z3, AST | Ethereum |
| Computing exact worst-case gas consumption for smart contracts | Marescotti et al. | ISoLA | 2018 | Resource consumption, Symbolic model checking, Solidity | Ethereum |
| SMT-friendly formalization of the Solidity memory model | Hajdu and Jovanović | ESOP | 2020 | Formal semantics, Memory model, solc-verify | Ethereum |
| Debugging smart contract's business logic using symbolic model-checking | Shishkin | Programming and Computer Software | 2019 | SMT solving, Z3, Symbolic model checker is under construction, Trace properties, Events | Ethereum |
| VeriSmart: A highly precise safety verifier for Ethereum smart contracts | So et al. | IEEE S&P | 2020 | Static analysis, Z3, Inductive invariants generation, CEGIS-style verification, Integer bugs | Ethereum |
| Formal verification of BNB smart contract | Li et al. | IEEE BIGCOM | 2019 | Process algebra, SAPIC, Tamarin prover, Invariants, BNB | Ethereum |
| Verification-led smart contracts | Banach | WTSC@FC | 2019 | Program synthesis, Set-based methods, Rodin, Event-B | Ethereum |
| Zkay: Specifying and enforcing data privacy in smart contracts | Steffen et al. | ACM CCS | 2019 | DSL, Privacy, NIZK proof | Ethereum |
| Town Crier: An authenticated data feed for smart contracts | Zhang et al. | ACM CCS | 2016 | Privacy, Trusted hardware, Inter SGX | Ethereum |
| Quantitative analysis of smart contracts | Chatterjee et al. | ESOP | 2018 | Game theory, Interval abstraction refinement, Bounded analysis, Objective function | Ethereum |
| MuSC: A tool for mutation testing of Ethereum smart contract | Li et al. | IEEE/ACM ASE | 2019 | Mutation-based testing, AST | Ethereum |
| Smart contract repair | Yu et al. | ACM TOSEM | 2020 | Mutation-based program repair, Code update, Resource consumption, SCRepair | Ethereum |
| Broken metre: Attacking resource metering in EVM | Perez and Livshits | NDSS | 2020 | Resource consumption, Exploit generation, Mutation-based program synthesis | Ethereum |
| Formal requirement enforcement on smart contracts based on Linear Dynamic Logic | Sato et al. | IEEE iThings, GreenCom, CPSCom, SmartData | 2018 | Program synthesis, Model сhecking, LDLf, ECA rules, Template, Statechart, SCXML | Hyperledger Fabric |
| Modeling Bitcoin contracts by timed automata | Andrychowicz et al. | FORMATS | 2014 | Model checking, UPPAAL, Timed automata, TCTL, Timed commitment | Bitcoin |
| Formal verification of smart contracts based on users and blockchain behaviors models | Abdellatif et al. | IFIP NTMS | 2018 | Model checking (statistical), BIP-SMC, BIP, Timed automata, PB-LTL, NameReg | Ethereum |
| Statistical model checking for blockchain-based applications | Maksimov et al. | IOP Conference Series: Materials Science and Engineering | 2020 | Model checking (statistical), BIP-SMC, BIP, Parametrized LTL, NameReg | N/A |
| Model checking smart contracts for Ethereum | Osterland and Rose | Pervasive and Mobile Computing | 2020 | Model Checking, SPIN, Promela, AST, Assertions | Ethereum |
| Formal modeling and verification of smart contracts | Bai et al. | ACM ICSCA | 2018 | Model checking, SPIN, Promela, LTL | N/A |
| Validation of decentralised smart contracts through game theory and formal methods | Bigi et al. | Programming Languages with Applications to Biology and Security | 2015 | Model checking, Prism, MDP, Strategic game, PCTL, BitHalo | Bitcoin |
| SolidWorx: A Resilient and Trustworthy Transactive Platform for Smart and Connected Communities | Eisele et al. | IEEE iThings, GreenCom, CPSCom, SmartData | 2018 | Program synthesis, Model checking, nuXmv, FSM, BIP, CTL | Ethereum |
| VeriSolid: Correct-by-design smart contracts for Ethereum | Mavridou et al. | WTSC@FC | 2019 | Program synthesis, FSolidM, Model checking, nuXmv, Design patterns, FSM, BIP, CTL | Ethereum |
| Verified development and deployment of multiple interacting smart contracts with VeriSolid | Nelaturu et al. | IEEE ICBC | 2020 | Program synthesis, FSolidM, Model checking, nuXmv, Design patterns, FSM, BIP, CTL | Ethereum |
| Policy specification and verification for blockchain and smart contracts in 5G networks | Unal et al. | ICT Express | 2019 | Model checking, NuSMV, Ambient calculus, Predicate logic, Access control, Wallet | N/A |
| Model-checking of smart contracts | Nehaı̈ et al. | IEEE iThings, GreenCom, CPSCom, SmartData | 2018 | Model checking, NuSMV, CTL, Energy marketplace | Ethereum |
| Formal verification of smart contracts using interface automata | Madl et al. | IEEE ICBC | 2019 | Model checking, NuSMV, Interface automata, CTL | Hyperledger Fabric |
| Formal verification of functional requirements for smart contract compositions in supply chain management systems | Alqahtani et al. | HICSS | 2020 | Model checking, NuSMV, FSM, BIP, LTL, Supply chain | Hyperledger Fabric |
| Securing smart contracts in blockchain | Kongmanee et al. | IEEE/ACM ASEW@ASE | 2019 | Model checking, NuSMV, Kripke structure, LTL | Ethereum |
| On the specification and verification of atomic swap smart contracts | Meyden | IEEE ICBC | 2019 | Model checking, MCK, Concurrent game structure, ATL, SL, Atomic swap | N/A (Cross-chain) |
| Developing secure Bitcoin contracts with BitML | Atzei et al. | ACM ESEC/FSE | 2019 | Model checking, Maude, BitML, LTL, Timed commitment | Bitcoin |
| Formal verification of smart contracts from the perspective of concurrency | Qu et al. | SmartBlock | 2018 | Process algebra, CSP, Model checking, FDR, Vulnerability | Ethereum |
| Formal analysis of smart contract based on Colored Petri Nets | Duo et al. | IEEE Intelligent Systems | 2020 | Model checking, cpntools, ASK-CTL, Hoare logic, EVM | Ethereum |
| Formal verification of blockchain smart contract based on Colored Petri Net models | Liu and Liu | IEEE COMPSAC | 2019 | Model checking, cpntools, ASK-CTL, Vulnerability | Ethereum |
| Verifying liquidity of Bitcoin contracts | Bartoletti and Zunino | POST | 2019 | Model checking, LTL, Liquidity | Bitcoin |
| S-gram: Towards semantic-aware security auditing for Ethereum smart contracts | Liu et al. | IEEE/ACM ASE | 2018 | Statistical language modeling, Vulnerabilities, AST, Solidity | Ethereum |
| Recommending differentiated code to support smart contract update | Huang et al. | IEEE/ACM ICPC | 2019 | Deep learning, Code embedding, Code update | Ethereum |
| Checking smart contracts with structural code embedding | Gao et al. | IEEE TSE | 2020 | Deep learning, Code embedding, AST, Clone detection, Bug detection, SmartEmbed | Ethereum |
| SmartEmbed: A tool for clone and bug detection in smart contracts through structural code embedding | Gao et al. | IEEE ICSME | 2019 | Deep learning, Code embedding, AST, Clone detection, Bug detection | Ethereum |
| Towards safer smart contracts: A sequence learning approach to detecting vulnerabilities | Tann et al. | arXiv | 2018 | Deep learning, Sequence learning, LSTM RNN model, EVM opcode, Vulnerabilities, Maian | Ethereum |
| Hunting the Ethereum smart contract: Color-inspired inspection of potential attacks | Huang | arXiv | 2018 | Deep learning, Transfer learning, RGB color code, Vulnerabilities, EVM bytecode | Ethereum |