Managing Timeouts

Certora Prover has a potential to run very long on some inputs. When it runs too long, it will give up and return a “timeout” (or in some cases “unknown”) result. In this chapter, we present a practical guide to diagnosing the causes of timeouts and ways to prevent them.

• Introduction
• Identifying timeout causes
  • Complexity feedback from Certora Prover
    • Difficulty statistics
    • Timeout TAC reports
    • Finding timeout causes through modularization
      • Sanity rules
      • Library contracts
• Timeout prevention
  • Prover settings
    • Dealing with a high path count
    • Dealing with nonlinear arithmetic
  • Modular verification
    • Library-based systems
  • Simplifying the source code
    • Passing complex structs
    • Memory and storage in inline assembly
• Timeouts in Certora Prover - Theoretical Background
  • Complexity of the SMT problem
  • Usefulness of worst-case intractable problems
  • Further reading