In order to check programs in an acceptable amount of time, the Prover simplifies the code being verified. This section describes the mechanisms for simplification.
The approximations described in this section may be underapproximations, meaning that they can cause real bugs to be overlooked by the Prover.
- Loop Unrolling
- Method Summarization
- Modeling of Hashing in the Prover
- Modeling the Keccak Function (bounded case)
- Hashing of Unbounded Data
- Background: The Solidity Storage Model