73 - VerX
VerX: is a verifier that can automatically prove temporal safety properties of Ethereum smart contracts.
The verifier is based on a careful combination of three ideas:
- Reduction of temporal safety verification to reachability checking
- An efficient symbolic execution engine used to compute precise symbolic states within a transaction
- Delayed abstraction which approximates symbolic states at the end of transactions into abstract states.
- Verification Tool
- Termporal Safety Properties
- Reduction: Temporal
- Safety -> Reachability
- Efficient Symbolic
- Checking Engine
- Delayed Abstraction