Pith. sign in

REVIEW 2 major objections 4 minor 68 references

VeriSmart: A Highly Precise Safety Verifier for Ethereum Smart Contracts

T0 review · 2 major / 4 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read VeriSmart claims to be the first smart-contract verifier that catches all arithmetic bugs in its benchmark (58 of 58 CVEs, 0.41% false alarms) by automatically discovering hidden transaction invariants.

desk verdict New CEGIS-style transaction invariant inference makes this a useful tool paper, but the 'exhaustive verification' claim breaks on reentrant external calls. read the letter →

arxiv 1908.11227 v2 pith:CE67ECMZ submitted 2019-08-29 cs.PL cs.CR

Sunbeom So , Myungho Lee , Jisu Park , Heejo Lee , Hakjoo Oh This is my paper · ORCID
classification cs.PLcs.CR
keywords EthereumsmartcontractsarithmeticsafetyintegeroverflowtransactioninvariantsCEGISverificationformalstaticanalysisSolidity
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

VeriSmart is a verifier for Ethereum smart contracts that aims to settle the arithmetic-safety question exhaustively: every integer over/underflow and division-by-zero should be found, and every clean operation should be proven safe, without a flood of false alarms. The paper claims this is achievable on real contracts, reporting 58 of 58 known CVEs detected with only 2 false positives out of 492 alarms, a 0.41% false positive rate. The decisive idea is to automatically discover transaction invariants — facts such as "the sum of all token balances equals the total supply" that remain true across arbitrary interleavings of transactions — and feed them back into the verification loop. If the claim holds, developers could run VeriSmart before deployment and trust an exhaustive answer rather than a heuristic bug report, greatly reducing manual auditing effort.

What carries the argument

The load-bearing object is the transaction invariant, a formula over global contract state that is established by the constructor and preserved by every public function no matter how transactions interleave. Around it, the algorithm builds a counterexample-guided inductive synthesis loop. The validator converts the contract annotated with a candidate invariant into basic paths, uses the strongest-postcondition transformer sp to produce verification conditions that check both the inductiveness of the invariant and the safety of each assertion, and hands unproven paths to the generator. The generator refines the transaction invariant and loop-invariant map by conjoining atomic predicates restricted to the forms x = y, x >= y, x = n, x >= n, x <= n, and sum(x) = e, where sum denotes the total value stored in a Solidity mapping. A preprocessing step expands sum-equality into case-split constraints over the indices that actually appear in the path, after which an SMT solver, helped by fast syntactic invalidity checks and domain-specific validity templates, discharges the conditions.

What would settle it

Take a contract where an external or non-inlined function changes a storage variable through a path VeriSmart's side-effect analysis does not track, such as a delegatecall, and use that change to make an addition overflow; if VeriSmart reports the contract safe, the exhaustive-verification claim is refuted.

Watch

Extended reading notes

Core claim

The central discovery is that the precision bottleneck for smart-contract verifiers is not the SMT solver but the absence of global, inter-transaction reasoning. VeriSmart observes that arithmetic operations in token-style contracts are usually safe only because of invariants that span all functions and all transactions — such as the sum of all balances equaling the total supply — and that these invariants are neither given by the programmer nor captured by standard abstract domains. The paper's algorithm adapts the counterexample-guided inductive synthesis (CEGIS) loop: a validator generates verification conditions annotated with a candidate transaction invariant and loop invariants, and a generator refines candidates by conjoining simple atomic predicates over variables and constants of the failing paths. This loop terminates with either a proof of safety or a list of potential violations, and the evaluation shows the discovered invariants are strong enough to prove safe the operations that two prior verifiers reported as alarms, and to expose six queries reported as CVE vulnerabilities as actually safe.

Load-bearing premise

VeriSmart's exhaustiveness depends on its analysis of which variables an external or non-inlined function call could change being complete; a single missed write could make the verifier certify a genuinely vulnerable contract as safe.

Editorial extensions

If this is right

  • Deployers can treat a VeriSmart 'safe' verdict as an exhaustive answer for arithmetic safety across all possible transaction orderings, not merely a single execution.
  • The six queries marked vulnerable by CVE reports but proven safe by VeriSmart would need to be removed from vulnerability databases, changing downstream security advisories.
  • Verification cost of roughly one hour for all 60 CVE contracts suggests a feasible pre-deployment checking cycle for token contracts.
  • Because the algorithm is property-agnostic, a new safety property can be checked by swapping the assertion generator, as demonstrated by the ownership-takeover case study.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • A natural extension is to let the generator propose quantified or disjunctive invariants; the two false alarms VeriSmart emits in benchmark #8 stem exactly from a quantifier-free restriction, so lifting it could remove even those.
  • The free-variable invalidity shortcut is a heuristic that can mislabel a valid condition as invalid, producing extra false alarms; a fallback that only skips the SMT call when the syntactic test is decisive would preserve speed without the approximation.
  • If transaction invariants are as decisive as the paper suggests, reentrancy and gas-limit analyses — which also need global state summaries across user calls — could inherit the same CEGIS machinery.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 4 minor

Summary. The paper presents VeriSmart, a CEGIS-style verifier for arithmetic safety of Ethereum smart contracts. The algorithm iteratively discovers transaction and loop invariants, verifies them via basic-path construction and verification-condition generation, and discharges VCs with an SMT solver augmented by domain-specific preprocessing and fast syntactic checks. The implementation is applied to the full Solidity language up to inline-assembly caveats, with function calls handled by inlining and conservative side-effect weakening. The evaluation on 60 CVE-affected contracts and 25 contracts from the Zeus dataset reports 100% recall on known arithmetic CVEs, a 0.41% false-positive rate on the CVE benchmark, and substantial improvements over six existing tools, with the tool and data publicly released.

Significance. If the exhaustiveness claim can be made sound, this is a significant contribution to smart-contract security analysis. The paper is the first to apply a CEGIS-style loop to the automatic discovery of transaction invariants, and the evaluation is unusually thorough: all 492 alarms and 484 unreported queries on the CVE benchmark were manually inspected, four incorrect CVE reports were identified, and the comparison includes both bug-finders and verifiers. The basic-path VC generation and the proof of Proposition 1 are standard and well presented. The main correctness risk lies in the abstraction of inter-contract calls under reentrancy, which, as argued in the major comments, can make the verifier certify a vulnerable contract as safe. The paper also ships a reproducible implementation and public datasets, which is a clear strength.

major comments (2)
  1. [§IV (Function Calls)] The treatment of inter-contract calls is not sound under standard EVM semantics. The paper states that 'inter-contract calls in Solidity cannot directly modify other contracts' states' and therefore only invalidates return variables at inter-contract call-sites. This ignores reentrancy: an external call o.foo() can invoke a public function or fallback of the caller, which may modify the caller's storage before control returns. The call-site formula is therefore left too strong; VeriSmart can prove an assertion safe on a path in which the external call does not modify caller globals, while a concrete transaction that reenters the caller violates the assertion. The separate analysis of the called contract with entry/exit true does not propagate the reentrant state change back to the caller's call-site formula. Because the paper's central claim is exhaustive verification of arithmetic safety, this is a load-bearing soundness gap. I recommend havocing all caller globals reachable through reentrant callbacks (or conservatively all globals) at external calls, or restricting the exhaustiveness claim to contracts that do not perform external calls to untrusted addresses.
  2. [§IV (Inline Assembly) and Abstract] The abstract and Section I claim that VeriSmart 'detect[s] all arithmetic bugs' and performs 'exhaustive verification', but the implementation supports the full Solidity language 'except for inline assembly', and the Inline Assembly paragraph states that VeriSmart 'may miss bugs hidden in embedded bytecode'. The side-effect replacement for assembly blocks is conservative only with respect to source-level variables, not with respect to arbitrary bytecode effects. These statements are in tension with the unconditional exhaustiveness claim. The claim should be scoped to 'all arithmetic bugs outside inline assembly', or the abstract and conclusion should be revised accordingly. This is not by itself a reason to reject, but it is part of the central claim and should be fixed.
minor comments (4)
  1. [§III-D (Efficient Invalidity Checking)] The free-variable test is a heuristic rather than a decision procedure, because it checks only condition (i) of Proposition 1. The paper correctly acknowledges that this may classify valid VCs as invalid, but the subsequent statement that the technique 'causes no false negatives' should be worded more carefully: it never certifies an unsafe query as safe, while it may create false alarms. Recommend presenting this as a precision-engineering technique with an explicit statement that the two ignored conditions are not checked.
  2. [Appendix A (Preprocessing)] The equisatisfiability claim for the replacement of sum(x)=e by G1∧G2 is asserted but not proved. A short proof, or at least an explicit statement of the assumptions about the domain of the mapping and the fresh variable Rx, would strengthen the appendix.
  3. [§V (Evaluation)] The manual classification of the 484 unalarmed queries as true negatives is central to the reported 100% recall, but the methodology is not described. Reporting the number of inspectors, the classification criteria, and any cases of disagreement would make this result more convincing, especially since Section V-D acknowledges that such classification can be subjective.
  4. [§II, Example 3] The proof sketch for the BTX contract relies on the transaction invariant ∑i balance[i] = 10000, but the invariant as stated is not inductive without also assuming that the summation does not overflow. The paper mentions this condition in prose but does not show how the CEGIS loop discovers the pair. A sentence connecting this example to the refinement relation of Section III-C would help the reader.

Circularity Check

0 steps flagged · score 0.0 of 10

No circular derivation: VeriSmart's claims rest on external CVE benchmarks and manual ground-truth inspection, not on self-referential fitting or self-citation.

full rationale

The paper is a tool/algorithm paper whose central claims are empirical. The verification algorithm (Section III) follows a standard CEGIS loop: the generator proposes candidate transaction and loop invariants from a domain-specific template set, and the validator checks inductiveness and safety with an SMT solver; there is no equation in which a predicted quantity is defined from a fitted quantity. The template set (x = y, x >= y, x = n, x >= n, x <= n, sum(x) = e) is a design choice motivated by observed Solidity patterns, not a parameter fitted to the evaluation contracts; the paper itself lists non-representativeness of benchmarks as a threat to validity (Section V-D), which is a generalizability concern rather than a circular reduction. The evaluation in Section V uses 60 externally assigned CVE reports and manual inspection of alarms; ground-truth corrections for four allegedly incorrect CVEs (Table III) were made after manual confirmation ('we manually confirmed that the CVE reports are actually incorrect'), not by accepting the tool's output as ground truth. No load-bearing self-citation appears: the references to prior work are external (e.g., CEGIS [13-15], side-effect analysis [25]) and do not supply the paper's uniqueness or correctness claims. The known limitation in Section IV that inter-contract calls are modeled without propagating reentrant state changes is a soundness/correctness risk and is explicitly acknowledged in the paper, but it is not an instance of a derivation reducing to its own inputs. Consequently, no step satisfies the quoted-equation reduction test for circularity.

Assumptions & free parameters 5 free parameters · 5 assumptions · 0 invented entities

The central claim depends on several hand-chosen engineering constants (inlining depth, timeouts, predicate templates) that affect precision, and on domain assumptions about Solidity semantics and the soundness of the side-effect analysis. No physical entities are invented; the 'sum' symbol is an internal abstraction for mapping sums. The main epistemic risk is that the invariant template set was designed from observations of real contracts and the evaluation uses the same contract population, so generalizability is not proven.

free parameters (5)
  • function_inlining_depth_k = 2 or less
    Calls are inlined only up to depth 2; larger or skipped functions are analyzed separately with conservative over-approximation, affecting precision and the false positive rate.
  • function_size_threshold = 20 statements
    Functions larger than 20 statements are not inlined; this is a hand-tuned engineering trade-off between scalability and precision.
  • verifier_timeout_for_last_loop_iteration = 1 minute
    Section V-A states the timeout is set to 1 minute for the last entrance of the CEGIS loop; lower values decrease precision.
  • z3_timeout = 10 seconds
    Per-query Z3 timeout; authors state lower values decrease precision (Section V-A, V-D).
  • refinement_atomic_predicate_set = x=y, x>=y, x=n, x>=n, x<=n, sum(x)=e
    The invariant search space is restricted to these quantifier-free linear predicates; this is the key hand-chosen domain-specific bias that makes the algorithm tractable, and it excludes the quantified and compound invariants responsible for the reported false positives (Section III-C, V-A).
assumptions (5)
  • domain assumption A Solidity contract's state evolves only through the constructor and public/external functions, all of which can be called from outside and may interleave arbitrarily.
    The transaction invariant is defined as a formula valid at end of constructor and preserved by every public function; this models reachable states without considering private/internal entry points or other entry mechanisms such as selfdestruct or block-embedded calls. Section III-A.
  • domain assumption The side-effect analysis used for function calls correctly over-approximates all variables that a called function may modify.
    Section IV (Function Calls) weakens call-site formulas by 'true' for every variable the side-effect analysis flags; if a modification is missed, the analysis is unsound (false negatives).
  • ad hoc to paper The syntactic free-variable check of Section III-D is an acceptable proxy for Proposition 1 in the target domain; in particular, the ignored conditions (ii) and (iii) are rarely violated in real smart contracts.
    The paper admits this heuristic can classify valid VCs as invalid, which is a source of false positives, and claims it caused none in the evaluation. This is not proven for arbitrary inputs.
  • ad hoc to paper The 'sum' function symbol denotes a summation that does not itself overflow, and the generated verification conditions faithfully encode that semantics.
    Appendix A translates sum(x)=e into equations with fresh variables plus overflow-freeness guards; the soundness of this encoding is argued informally and is central to the precision results.
  • standard math The underlying SMT solver (Z3) is assumed correct.
    The validator delegates validity checking to Z3 after preprocessing; the paper assumes Z3's bitvector/array theory solvers are sound.

how reviews work

0 comments
Cite this review

Pith. "Pith review of VeriSmart: A Highly Precise Safety Verifier for Ethereum Smart Contracts." pith.science (2026). https://pith.science/paper/CE67ECMZ

@misc{pith2026190811227,
  author       = {Pith},
  title        = {Pith review of: VeriSmart: A Highly Precise Safety Verifier for Ethereum Smart Contracts},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/CE67ECMZ}},
  note         = {Machine review of arXiv:1908.11227}
}
read the original abstract

We present VeriSmart, a highly precise verifier for ensuring arithmetic safety of Ethereum smart contracts. Writing safe smart contracts without unintended behavior is critically important because smart contracts are immutable and even a single flaw can cause huge financial damage. In particular, ensuring that arithmetic operations are safe is one of the most important and common security concerns of Ethereum smart contracts nowadays. In response, several safety analyzers have been proposed over the past few years, but state-of-the-art is still unsatisfactory; no existing tools achieve high precision and recall at the same time, inherently limited to producing annoying false alarms or missing critical bugs. By contrast, VeriSmart aims for an uncompromising analyzer that performs exhaustive verification without compromising precision or scalability, thereby greatly reducing the burden of manually checking undiscovered or incorrectly-reported issues. To achieve this goal, we present a new domain-specific algorithm for verifying smart contracts, which is able to automatically discover and leverage transaction invariants that are essential for precisely analyzing smart contracts. Evaluation with real-world smart contracts shows that VeriSmart can detect all arithmetic bugs with a negligible number of false alarms, far outperforming existing analyzers.

Figures

Figures reproduced from arXiv: 1908.11227 by the authors.

Figure 1
Figure 1. A vulnerable function from SmartMesh (CVE-2018-10376). [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. A vulnerable function from Neo Genesis Token (CVE-2018-14006). [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. Example contract simplified from CVE-2018-13326. [PITH_FULL_IMAGE:figures/full_fig_p003_3.png] view at source ↗
Figures from the paper (3 more)
Figure 4
Figure 4. Figure 4: Example contract. Generator unproven queries candidate invariants Solidity Program Verification Result Validator Solver [PITH_FULL_IMAGE:figures/full_fig_p004_4.png]
Figure 5
Figure 5. Figure 5: Algorithm overview. Invariants of Smart Contracts: We consider two kinds of invariants for smart contracts: transaction and loop invariants. We say a formula is a transaction invariant if it is valid at the end of the constructor and the validity is preserved by the ex…
Figure 6
Figure 6. Figure 6: A function simplified from the benchmark #8. O [PITH_FULL_IMAGE:figures/full_fig_p011_6.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

68 extracted references · 48 canonical work pages

  1. [1]

    [Online]

    2018, [Online; accessed 31-May-2019]. [Online]. Available: http: //virtual-strategy.com/2018/12/05/hashcash-enters- malta-with-smart- contract-based-insurance-automation/

    work page 2018

  2. [2]

    Smart Contracts for Machine-to-Machine Communication: Possibilities and Limitations

    Y . Hanada, L. Hsiao, and P. Levis, “Smart contracts for machine- to-machine communication: Possibilities and limitations,” CoRR, vol. abs/1806.00555, 2018. [Online]. Available: http://arxiv.org/abs/1806. 00555

    work page Pith review arXiv 2018

  3. [3]

    A survey of attacks on ethereum smart contracts sok,

    N. Atzei, M. Bartoletti, and T. Cimoli, “A survey of attacks on ethereum smart contracts sok,” in Proceedings of the 6th International Conference on Principles of Security and Trust - Volume 10204 . New York, NY , USA: Springer-Verlag New York, Inc., 2017, pp. 164–186. [Online]. Available: https://doi.org/10.1007/978-3-662-54455-6 8

    doi:10.1007/978-3-662-54455-6 2017

  4. [4]

    [Online]

    2016, [Online; accessed 31-May-2019]. [Online]. Available: https: //www.wired.com/2016/06/50-million-hack-just-showed-dao-human/

    work page 2016

  5. [5]

    [Online]

    2018, [Online; accessed 31-May-2019]. [Online]. Available: https://blockexplorer.com/news/260-million-parity-proposes-eip-999- to-recover-frozen-multi-sig-funds/

    work page 2018

  6. [6]

    [Online]

    2018, [Online; accessed 31-May-2019]. [Online]. Available: https: //blog.peckshield.com/2018/04/25/proxyOverflow/

    work page 2018

  7. [8]

    Mythril classic: an open-source security analysis tool for ethereum smart contracts

    “Mythril classic: an open-source security analysis tool for ethereum smart contracts.” 2018, [Online; accessed 31-May-2019]. [Online]. Available: https://github.com/ConsenSys/mythril-classic

    work page 2018

  8. [9]

    Making smart contracts smarter,

    L. Luu, D.-H. Chu, H. Olickel, P. Saxena, and A. Hobor, “Making smart contracts smarter,” in Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security , ser. CCS ’16. New York, NY , USA: ACM, 2016, pp. 254–269. [Online]. Available: http://doi.acm.org/10.1145/2976749.2978309

    arXiv 2016

Show all 68 references
  1. [10]

    Manticore: a symbolic execution tool for analysis of smart contracts and binaries,

    “Manticore: a symbolic execution tool for analysis of smart contracts and binaries,” 2017, [Online; accessed 31-May-2019]. [Online]. Available: https://github.com/trailofbits/manticore

    2017

  2. [11]

    ZEUS: analyzing safety of smart contracts,

    S. Kalra, S. Goel, M. Dhawan, and S. Sharma, “ZEUS: analyzing safety of smart contracts,” in 25th Annual Network and Distributed System Security Symposium, NDSS 2018, San Diego, California, USA, February 18-21, 2018. The Internet Society, 2018. [Online]. Available: http://wp.i...

    2018

  3. [12]

    Smt-based verification of solidity smart contracts,

    L. Alt and C. Reitwiessner, “Smt-based verification of solidity smart contracts,” in Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice , T. Margaria and B. Steffen, Eds. Cham: Springer International Publishing, 2018, pp. 376–388

    2018

  4. [13]

    Combinatorial sketching for finite programs,

    A. Solar-Lezama, L. Tancau, R. Bodik, S. Seshia, and V . Saraswat, “Combinatorial sketching for finite programs,” SIGOPS Oper. Syst. Rev., vol. 40, no. 5, pp. 404–415, Oct. 2006. [Online]. Available: http://doi.acm.org/10.1145/1168917.1168907

    2006

  5. [14]

    Transit: Specifying protocols with concolic snippets,

    A. Udupa, A. Raghavan, J. V . Deshmukh, S. Mador-Haim, M. M. Martin, and R. Alur, “Transit: Specifying protocols with concolic snippets,” in Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation , ser. PLDI ’13. New York, NY , USA: AC...

    2013

  6. [15]

    Program synthesis by sketching,

    A. Solar-Lezama, “Program synthesis by sketching,” Ph.D. dissertation, Berkeley, CA, USA, 2008, aAI3353225

    2008

  7. [16]

    [Online]

    2018, [Online; accessed 31-May-2019]. [Online]. Available: https: //github.com/VenusADLab/EtherTokens/blob/master/SHARKTECH/ SHARKTECH.md

    2018

  8. [17]

    Solidity 0.5.3,

    “Solidity 0.5.3,” 2019, [Online; accessed 31-May-2019]. [Online]. Available: https://solidity.readthedocs.io/en/v0.5.3/index.html

    2019

  9. [18]

    Finding the greedy, prodigal, and suicidal contracts at scale,

    I. Nikoli ´c, A. Kolluri, I. Sergey, P. Saxena, and A. Hobor, “Finding the greedy, prodigal, and suicidal contracts at scale,” in Proceedings of the 34th Annual Computer Security Applications Conference , ser. ACSAC ’18. New York, NY , USA: ACM, 2018, pp. 653–663. [Online]. Av...

    2018

  10. [19]

    Securify: Practical security analysis of smart contracts,

    P. Tsankov, A. Dan, D. Drachsler-Cohen, A. Gervais, F. B ¨unzli, and M. Vechev, “Securify: Practical security analysis of smart contracts,” in Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security , ser. CCS ’18. New York, NY , USA: ACM, 2018, p...

    2018

  11. [20]

    Madmax: Surviving out-of-gas conditions in ethereum smart contracts,

    N. Grech, M. Kong, A. Jurisevic, L. Brent, B. Scholz, and Y . Smaragdakis, “Madmax: Surviving out-of-gas conditions in ethereum smart contracts,” Proc. ACM Program. Lang. , vol. 2, no. OOPSLA, pp. 116:1–116:27, Oct. 2018. [Online]. Available: http://doi.acm.org/10.1145/3276486

    2018 doi

  12. [21]

    Vandal: A scalable security analysis framework for smart contracts,

    L. Brent, A. Jurisevic, M. Kong, E. Liu, F. Gauthier, V . Gramoli, R. Holz, and B. Scholz, “Vandal: A scalable security analysis framework for smart contracts,” CoRR, vol. abs/1809.03981, 2018

    2018 arXiv

  13. [22]

    A. R. Bradley and Z. Manna, The Calculus of Computation: Decision Procedures with Applications to Verification . Berlin, Heidelberg: Springer-Verlag, 2007

    2007

  14. [23]

    Z3: An efficient smt solver,

    L. de Moura and N. Bjørner, “Z3: An efficient smt solver,” in Tools and Algorithms for the Construction and Analysis of Systems , C. R. Ramakrishnan and J. Rehof, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2008, pp. 337–340

    2008

  15. [24]

    Barrett, C

    C. Barrett, C. L. Conway, M. Deters, L. Hadarean, D. Jovanovi’c, T. King, A. Reynolds, and C. Tinelli, “CVC4,” in Proceedings of the 23rd International Conference on Computer Aided Verification (CAV ’11), ser. Lecture Notes in Computer Science, G. Gopalakrishnan and S. Qadeer, ...

    2011

  16. [25]

    Interprocedural side-effect analysis in linear time,

    K. D. Cooper and K. Kennedy, “Interprocedural side-effect analysis in linear time,” in Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation , ser. PLDI ’88. New York, NY , USA: ACM, 1988, pp. 57–66. [Online]. Available: http://doi.ac...

    1988

  17. [26]

    Oyente: An analysis tool for smart contracts,

    “Oyente: An analysis tool for smart contracts,” 2018, [Online; accessed 31-May-2019]. [Online]. Available: https://github.com/melonproject/ oyente

    2018

  18. [27]

    Etherscan,

    “Etherscan,” [Online; accessed 31-May-2019]. [Online]. Available: https://etherscan.io/

    2019

  19. [28]

    Zeus evaluation,

    “Zeus evaluation,” 2018, [Online; accessed 31-May-2019]. [Online]. Available: https://goo.gl/kFNHy3

    2018

  20. [29]

    [Online]

    [Online; accessed 31-May-2019]. [Online]. Available: https://github. com/ethereum/solidity/issues/6835

    2019

  21. [30]

    [Online]

    [Online; accessed 31-May-2019]. [Online]. Available: https://blog. peckshield.com/2018/05/21/ceoAnyone/

    2019

  22. [31]

    Under-optimized smart contracts devour your money,

    T. Chen, X. Li, X. Luo, and X. Zhang, “Under-optimized smart contracts devour your money,” in 2017 IEEE 24th International Conference on Software Analysis, Evolution and Reengineering (SANER) , Feb 2017, pp. 442–446

    2017

  23. [32]

    GASTAP: A gas analyzer for smart contracts,

    E. Albert, P. Gordillo, A. Rubio, and I. Sergey, “GASTAP: A gas analyzer for smart contracts,” CoRR, vol. abs/1811.10403, 2018. [Online]. Available: http://arxiv.org/abs/1811.10403

    2018 arXiv

  24. [33]

    Online detection of effectively callback free objects with applications to smart contracts,

    S. Grossman, I. Abraham, G. Golan-Gueta, Y . Michalevsky, N. Rinetzky, M. Sagiv, and Y . Zohar, “Online detection of effectively callback free objects with applications to smart contracts,” Proc. ACM Program. Lang., vol. 2, no. POPL, pp. 48:1–48:28, Dec. 2017. [Online]. Availa...

    2017 doi

  25. [34]

    Reguard: Finding reentrancy bugs in smart contracts,

    C. Liu, H. Liu, Z. Cao, Z. Chen, B. Chen, and B. Roscoe, “Reguard: Finding reentrancy bugs in smart contracts,” in 2018 IEEE/ACM 40th International Conference on Software Engineering: Companion (ICSE- Companion), May 2018, pp. 65–68

    2018

  26. [35]

    Formal verification for solidity contracts

    C. Reitwiessner, “Formal verification for solidity contracts.” 2015, [Online; accessed 31-May-2019]. [Online]. Available: https://forum. ethereum.org/discussion/3779/formal-verification-for-solidity-contracts

    2015

  27. [36]

    Defining the ethereum virtual machine for interactive theorem provers,

    Y . Hirai, “Defining the ethereum virtual machine for interactive theorem provers,” in Financial Cryptography and Data Security , M. Brenner, K. Rohloff, J. Bonneau, A. Miller, P. Y . Ryan, V . Teague, A. Bracciali, M. Sala, F. Pintore, and M. Jakobsson, Eds. Cham: Springer Int...

    2017

  28. [37]

    Formal verification of smart contracts: Short paper,

    K. Bhargavan, A. Delignat-Lavaud, C. Fournet, A. Gollamudi, G. Gonthier, N. Kobeissi, N. Kulatova, A. Rastogi, T. Sibut-Pinote, N. Swamy, and S. Zanella-B ´eguelin, “Formal verification of smart contracts: Short paper,” in Proceedings of the 2016 ACM Workshop on Programming Lan...

    2016

  29. [38]

    A semantic frame- work for the security analysis of ethereum smart contracts,

    I. Grishchenko, M. Maffei, and C. Schneidewind, “A semantic frame- work for the security analysis of ethereum smart contracts,” inPrinciples of Security and Trust , L. Bauer and R. K ¨usters, Eds. Cham: Springer International Publishing, 2018, pp. 243–269

    2018

  30. [39]

    Towards verifying ethereum smart contract bytecode in isabelle/hol,

    S. Amani, M. B ´egel, M. Bortin, and M. Staples, “Towards verifying ethereum smart contract bytecode in isabelle/hol,” in Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs , ser. CPP 2018. New York, NY , USA: ACM, 2018, pp. 66–77. [Onl...

    2018 doi

  31. [40]

    Formal specification and verification of smart contracts for azure blockchain,

    S. K. Lahiri, S. Chen, Y . Wang, and I. Dillig, “Formal specification and verification of smart contracts for azure blockchain,” CoRR, vol. abs/1812.08829, 2018. [Online]. Available: http://arxiv.org/abs/1812. 08829

    2018 arXiv

  32. [41]

    Contractfuzzer: fuzzing smart contracts for vulnerability detection,

    B. Jiang, Y . Liu, and W. K. Chan, “Contractfuzzer: fuzzing smart contracts for vulnerability detection,” in ASE. ACM, 2018, pp. 259– 269

    2018

  33. [42]

    The seahorn verification framework,

    A. Gurfinkel, T. Kahsai, A. Komuravelli, and J. A. Navas, “The seahorn verification framework,” in Computer Aided Verification , D. Kroening and C. S. P ˘as˘areanu, Eds. Cham: Springer International Publishing, 2015, pp. 343–361

    2015

  34. [43]

    Strictly declarative specification of sophisticated points-to analyses,

    M. Bravenboer and Y . Smaragdakis, “Strictly declarative specification of sophisticated points-to analyses,” in Proceedings of the 24th ACM SIGPLAN Conference on Object Oriented Programming Systems Languages and Applications , ser. OOPSLA ’09. New York, NY , USA: ACM, 2009, pp....

    2009

  35. [44]

    Nipkow, M

    T. Nipkow, M. Wenzel, and L. C. Paulson, Isabelle/HOL: A Proof Assistant for Higher-order Logic . Berlin, Heidelberg: Springer-Verlag, 2002

    2002

  36. [45]

    Dependent types and multi- monadic effects in F*,

    N. Swamy, C. Hritcu, C. Keller, A. Rastogi, A. Delignat-Lavaud, S. Forest, K. Bhargavan, C. Fournet, P.-Y . Strub, M. Kohlweiss, J.-K. Zinzindohou´e, and S. Zanella-B ´eguelin, “Dependent types and multi- monadic effects in F*,” in 43rd ACM SIGPLAN-SIGACT Symposium on Principl...

    2016

  37. [46]

    Kevm: A complete formal semantics of the ethereum virtual machine,

    E. Hildenbrandt, M. Saxena, N. Rodrigues, X. Zhu, P. Daian, D. Guth, B. Moore, D. Park, Y . Zhang, A. Stefanescu, and G. Rosu, “Kevm: A complete formal semantics of the ethereum virtual machine,” in 2018 IEEE 31st Computer Security Foundations Symposium (CSF), July 2018, pp. 204–217

    2018

  38. [47]

    An overview of the K semantic frame- work,

    G. Ros ¸u and T. F. S ¸erb˘anut ¸˘a, “An overview of the K semantic frame- work,” Journal of Logic and Algebraic Programming, vol. 79, no. 6, pp. 397–434, 2010

    2010

  39. [48]

    Openzeppelin: Safemath,

    “Openzeppelin: Safemath,” 2018, [Online; accessed 31-May-2019]. [Online]. Available: https://github.com/OpenZeppelin/openzeppelin- solidity/blob/master/contracts/math/SafeMath.sol

    2018

  40. [49]

    A static analyzer for large safety-critical software,

    B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Min ´e, D. Monniaux, and X. Rival, “A static analyzer for large safety-critical software,” in Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation , ser. PLDI ’03. New Yor...

    2003

  41. [50]

    Why does astr ´ee scale up?

    P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Min ´e, and X. Rival, “Why does astr ´ee scale up?” Formal Methods in System Design, vol. 35, no. 3, pp. 229–264, 2009. [Online]. Available: https://doi.org/10.1007/s10703-009-0089-6

    2009 doi

  42. [51]

    Sparrow,

    “Sparrow,” [Online; accessed 31-May-2019]. [Online]. Available: https://github.com/ropas/sparrow

    2019

  43. [52]

    Frama-c: A software analysis perspective,

    F. Kirchner, N. Kosmatov, V . Prevosto, J. Signoles, and B. Yakobowski, “Frama-c: A software analysis perspective,” Formal Asp. Comput. , vol. 27, no. 3, pp. 573–609, 2015. [Online]. Available: https: //doi.org/10.1007/s00165-014-0326-7

    2015 doi

  44. [53]

    Frama-c: a source-code analyzer of c software

    “Frama-c: a source-code analyzer of c software.” [Online; accessed 31-May-2019]. [Online]. Available: https://frama-c.com/index.html

    2019

  45. [54]

    Improving integer security for systems with kint,

    X. Wang, H. Chen, Z. Jia, N. Zeldovich, and M. F. Kaashoek, “Improving integer security for systems with kint,” in Proceedings of the 10th USENIX Conference on Operating Systems Design and Implementation , ser. OSDI’12. Berkeley, CA, USA: USENIX Association, 2012, pp. 163–177....

    2012

  46. [55]

    Intscope: Automatically detecting integer overflow vulnerability in X86 binary using symbolic execution,

    T. Wang, T. Wei, Z. Lin, and W. Zou, “Intscope: Automatically detecting integer overflow vulnerability in X86 binary using symbolic execution,” in Proceedings of the Network and Distributed System Security Symposium, NDSS 2009, San Diego, California, USA, 8th February - 11th Fe...

    2009

  47. [56]

    Dynamic test generation to find integer bugs in x86 binary linux programs,

    D. Molnar, X. C. Li, and D. A. Wagner, “Dynamic test generation to find integer bugs in x86 binary linux programs,” in Proceedings of the 18th Conference on USENIX Security Symposium , ser. SSYM’09. Berkeley, CA, USA: USENIX Association, 2009, pp. 67–82. [Online]. Available: ht...

    2009

  48. [57]

    Modular bug-finding for integer overflows in the large: Sound, efficient, bit-precise static analysis,

    Y . Moy, N. Bjørner, and D. Sielaff, “Modular bug-finding for integer overflows in the large: Sound, efficient, bit-precise static analysis,” Tech. Rep. MSR-TR-2009–57, 2009

    2009

  49. [58]

    Targeted automatic integer overflow discovery using goal-directed conditional branch enforcement,

    S. Sidiroglou-Douskos, E. Lahtinen, N. Rittenhouse, P. Piselli, F. Long, D. Kim, and M. Rinard, “Targeted automatic integer overflow discovery using goal-directed conditional branch enforcement,” in Proceedings of the Twentieth International Conference on Architectural Support ...

    2015

  50. [59]

    Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints,

    P. Cousot and R. Cousot, “Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints,” in Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages , ser. POPL ’77. New York, NY ...

    1977

  51. [60]

    Systematic design of program analysis frameworks,

    ——, “Systematic design of program analysis frameworks,” in Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages , ser. POPL ’79. New York, NY , USA: ACM, 1979, pp. 269–282. [Online]. Available: http://doi.acm.org/10.1145/567752.567778

    1979

  52. [61]

    The octagon abstract domain,

    A. Min ´e, “The octagon abstract domain,” Higher-Order and Symbolic Computation, vol. 19, no. 1, pp. 31–100, 2006. [Online]. Available: https://doi.org/10.1007/s10990-006-8609-1

    2006 doi

  53. [62]

    A tool for checking ansi-c programs,

    E. Clarke, D. Kroening, and F. Lerda, “A tool for checking ansi-c programs,” in Tools and Algorithms for the Construction and Analysis of Systems, K. Jensen and A. Podelski, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2004, pp. 168–176

    2004

  54. [63]

    How to avoid proving the absence of integer overflows,

    M. Clochard, J.-C. Filli ˆatre, and A. Paskevich, “How to avoid proving the absence of integer overflows,” in Verified Software: Theories, Tools, and Experiments, A. Gurfinkel and S. A. Seshia, Eds. Cham: Springer International Publishing, 2015, pp. 94–109

    2015

  55. [64]

    Flow-insensitive static analysis for detecting integer anomalies in programs,

    D. Sarkar, M. Jagannathan, J. Thiagarajan, and R. Venkatapathy, “Flow-insensitive static analysis for detecting integer anomalies in programs,” in Proceedings of the 25th Conference on IASTED International Multi-Conference: Software Engineering , ser. SE’07. Anaheim, CA, USA: ...

    2007

  56. [65]

    Using type qualifiers to analyze untrusted integers and detecting security flaws in c programs,

    E. N. Ceesay, J. Zhou, M. Gertz, K. Levitt, and M. Bishop, “Using type qualifiers to analyze untrusted integers and detecting security flaws in c programs,” in Detection of Intrusions and Malware & Vulnerability Assessment, R. B ¨uschkes and P. Laskov, Eds. Berlin, Heidelberg: S...

    2006

  57. [66]

    Sound input filter generation for integer overflow errors,

    F. Long, S. Sidiroglou-Douskos, D. Kim, and M. Rinard, “Sound input filter generation for integer overflow errors,” in Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ser. POPL ’14. New York, NY , USA: ACM, 2014, pp. 439–

    2014

  58. [67]

    Program transformations to fix c integers,

    Z. Coker and M. Hafiz, “Program transformations to fix c integers,” in Proceedings of the 2013 International Conference on Software Engineering, ser. ICSE ’13. Piscataway, NJ, USA: IEEE Press, 2013, pp. 792–801. [Online]. Available: http://dl.acm.org/citation.cfm?id= 2486788.2486892

    2013

  59. [68]

    Intpti: Automatic integer error repair with proper-type inference,

    X. Cheng, M. Zhou, X. Song, M. Gu, and J. Sun, “Intpti: Automatic integer error repair with proper-type inference,” in Proceedings of the 32Nd IEEE/ACM International Conference on Automated Software Engineering , ser. ASE 2017. Piscataway, NJ, USA: IEEE Press, 2017, pp. 996–10...

    2017

  60. [452]

    Available: http://doi.acm.org/10.1145/2535838.2535888

    [Online]. Available: http://doi.acm.org/10.1145/2535838.2535888

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.