runtimeverification / runtimeverification/kontrol
Make CSE more useful by reusing the previous proof
Open
@Stevengre is already working on this.
Since Nov 27, 2024.
cse
- Dominant language
- Python
- Stars
- 122
- Forks
- 16
- PR merge metrics
- No merged PRs in 30d
Description
Currently, the proof will re-run all the things when using --reinit and unchange if there is a proof. Therefore, the CSE won't bring a lot of improvement for the tests which just call a function once.
My idea is to provide incremental verification: If only the tests changes, don't re-generate the summary for the external callee functions. Intead, use the summary directly. I think this will significantly enhance the verification experience, especially in scenarios where only the tests will be modified during the audit.
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Assessment
This issue has not been assessed yet.