Certora Prover Documentation
latest

Contents

  • Certora Technology White Paper
  • Certora User’s Guide
  • The Certora Verification Language
  • The Certora Prover
  • Gambit: Mutation Generator for Solidity
  • Equivalence Checking Using the Certora Prover
  • Old Documentation
    • Specification By Example
    • The Anatomy of a Specification
    • Advanced Subjects
      • Method declarations
      • Summarizing Solidity Functions
      • Internal Function Summaries
      • More Expressive Summaries
      • Multicontract
      • Linking Contracts
      • Approximation
      • Advanced Debugging
      • Grounding
    • Best Practices
    • Common Pitfalls
    • Assert splitting
    • Troubleshooting
Certora Prover Documentation
  • »
  • Old Documentation »
  • Advanced Subjects
  • Edit on GitHub

Advanced Subjects

  • Method declarations
  • Summarizing Solidity Functions
    • Calls inside the code
  • Internal Function Summaries
    • Allowed Summaries
    • Example
  • More Expressive Summaries
    • Ghost Summaries
    • CVL Function Summaries
  • Multicontract
  • Linking Contracts
  • Approximation
    • The Problem
    • Solution 1: Overapproximation
      • Uninterpreted Function as an Overapproximation
      • Axiomatized Uninterpreted Function as an Overapproximation
  • Advanced Debugging
    • Memory Analysis
  • Grounding
    • Flag
    • Grounding General Idea
    • Limitations
      • Alternating Quantifiers
      • Recursion
      • Variables That Are Not Arguments
      • Double Polarity
      • Simple Parameters
Previous Next

© Copyright 2022, Certora, Inc. Revision 19a6cd2f.

Built with Sphinx using a theme provided by Read the Docs.
Read the Docs v: latest
Versions
latest
cvl1
Downloads
On Read the Docs
Project Home
Builds