Managing Timeouts and Out of Memory Problems

In this chapter, we describe how to diagnose and remedy when the Certora Prover ran out of time or out of memory.

Out-of-memory problems are signified by an Extremely low available memory message in the Global Problems tab of the Prover reports, see Out of memory problems for more details. Timeouts are signified either by a Global timeout reached message in the Global Problems tab, if the whole Prover job timed out, or by an orange clock symbol next to the rule, if that particular rule timed out, see Timeouts for more details.

• Out of memory problems
  • General indicators
  • Reducing memory usage
    • High memory usage of SMT solvers
• Timeouts
  • Classification of Timeouts
  • Identifying timeout causes
    • Complexity feedback from Certora Prover
      • Difficulty statistics
      • Timeout TAC reports
      • Finding timeout causes through modularization
        • Sanity rules
        • Library contracts
  • Timeout prevention
    • Running rules individually
    • Detect candidates for summarization
      • Example usage
    • Dealing with different kinds of complexity
      • Dealing with a high path count
        • Path explosion
        • Mitigation approaches
      • Dealing with nonlinear arithmetic
      • Dealing with high memory (or storage) complexity
        • Passing complex structs
        • Memory and storage in inline assembly
    • Modular verification
      • Library-based systems
    • Command line options
      • --prover_args '-destructiveOptimizations enable'
• Timeouts in Certora Prover - Theoretical Background
  • Complexity of the SMT problem
  • Usefulness of worst-case intractable problems
  • Further reading