Run boogie in parallel with different solvers

SRI-CSL / solidity

This is solc-verify, a modular verifier for Solidity.

https://github.com/SRI-CSL/solidity/blob/boogie/SOLC-VERIFY-README.md

GNU General Public License v3.0

50 stars 14 forks source link

Run boogie in parallel with different solvers #145

Closed dddejan closed 4 years ago

dddejan commented 4 years ago

For usability, it would be preferable to check procedures individually and run in parallel with different solvers. This can be done with boogie /proc:<p> option that selects which procedure to check.

The workflow would be:

Compiler produces BPL and list of procedures to analyze
For each procedure to analyze run all boogie/solver combination with timeout, take fastest result, kill others.

dddejan commented 4 years ago

I did a first draft of per-procedure verification in merge branch. Next step to cleanup to the point where we can run multiple solvers.

dddejan commented 4 years ago

Closing this for now. Needs improvements, but will work it out separately.