mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
388 B
388 B
The Solidity compiler implements several optimization rules.
This directory contains an effort to formally prove the correctness of those rules in:
- HOL with EthIsabelle
- FOL with SMT solvers using Integers and BitVectors