Closed pirapira closed 7 years ago
In https://github.com/ethereum/solidity/issues/1178 there is a plan to export annotated opcodes from the Solidity compiler.
This issue keeps track of performing an experiment of verifying a program snippet with interleaved static assertions. See the proposed syntax in https://github.com/ethereum/solidity/issues/1178.
This has been done in the Isabelle/HOL repository.
pirapira
commented
7 years ago
In https://github.com/ethereum/solidity/issues/1178 there is a plan to export annotated opcodes from the Solidity compiler.
This issue keeps track of performing an experiment of verifying a program snippet with interleaved static assertions. See the proposed syntax in https://github.com/ethereum/solidity/issues/1178.