Publications

Publications related to solc-verify

Note that the Solidity language and solc-verify is also changing rapidly. For up-to-date information, always check out the readme on the appropriate branch of the repository.

Papers and talks

• FMBC 2020: Formal Specification and Verification of Solidity Contracts with Events [PDF] [Talk]
  Extending the specification and verification capabilities to reason about contracts with events.
• Solidity Summit 2020: solc-verify, a source-level formal verification tool for Solidity smart contracts [Talk] [Demo]
  A developer-oriented demo and talk on the usage of the tool.
• ESOP 2020: SMT-Friendly Formalization of the Solidity Memory Model [PDF] [Talk] [Tests]
  Formalization of reference types (e.g., arrays, mappings, structs) and the memory model (storage and memory data locations).
  • Also presented at SMT 2020 [Talk]
  • Also presented at WoSCA 2020 [Talk]
• VSTTE 2019: solc-verify: A Modular Verifier for Solidity Smart Contracts [PDF]
  An overview of the modular verification approach including the specification annotations and the translation to Boogie.
  • An extended version can be found in Chapter 3 of the PhD dissertation of Ákos Hajdu [PDF]

Citation

To cite solc-verify (as a tool), please use

@incollection{solcverify,
    author     = {Hajdu, {\'A}kos and Jovanovi{\'c}, Dejan},
    title      = {solc-verify: A Modular Verifier for {S}olidity Smart Contracts},
    year       = {2020},
    booktitle  = {Verified Software. Theories, Tools, and Experiments},
    series     = {Lecture Notes in Computer Science},
    volume     = {12301},
    publisher  = {Springer},
    editor     = {Chakraborty, Supratik and Navas, Jorge A.},
    pages      = {161-179},
    isbn       = {978-3-030-41600-3},
    doi        = {10.1007/978-3-030-41600-3_11},
}