Skip to content

Solicitous, the CHC verifier for Solidity contracts

License

Notifications You must be signed in to change notification settings

shrike71/solc

 
 

Solicitous, the CHC verifier for Solidity contracts

Solicitous is a module of the SMTChecker component of the Solidity compiler. For build instructions please follow the official repository (https://github.com/ethereum/solidity). This is the v0.6 implementation used in the experiments of our ISoLA 2020 paper, active develepment of Solicitous is done in the official repository under the branches prefixed with smt_.

To enable SMTChecker add pragma experimental SMTChecker; to the source file being checked, while having Z3 installed. Detailed information can be found in the official documentation (https://solidity.readthedocs.io/en/latest/security-considerations.html?#formal-verification).

About

Solicitous, the CHC verifier for Solidity contracts

Resources

License

Code of conduct

Security policy

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages

  • C++ 71.2%
  • Solidity 23.8%
  • Shell 2.1%
  • CMake 1.0%
  • C 0.8%
  • Python 0.7%
  • Other 0.4%