-
Notifications
You must be signed in to change notification settings - Fork 12
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Multi-property solving #30
Comments
This can be done with not too much work, depending on the engine used. There is a question of how to interact with the user in this case, with the user potentially being another program, e.g. how to report that a specific property is valid or a counter-example is found. Do you have any problems you can share for the multi-property checking? |
Here's an example of a multi-property file where lemmas are needed to prove a property: https://gist.github.com/agacek/ad0b3513b0e78b47995b Here lemmaA is hard to prove on its own, but easy if you conjoin it with lemmaB (or lemmaC even). Moreover, the ok1 property is much easier if conjoined with lemmaA, lemmaB, and lemmaC. Playing with this file also exposed another strange result in sally. Consider these two queries for the transition system given in the file.
Using k-induction, the first query is proved instantly. Sally then gets stuck on the second property. But the second property is an immediate consequence of the first. Sally should be using previously proven results as invariants for proving future properties. I have no strong feelings about the UI / API. |
Sally seems to process process queries sequentially. For k-induction, it's often beneficial to attack problems simultaneously so that they can be used to strengthen each other. We can simulate this by just conjoining all of our properties, but if any one of them is false then the whole property becomes false.
Something like the "Multi-property incremental verification" from "Incremental verification with mode variable invariants in state machines" by Kahsai, et al. would be very useful.
The text was updated successfully, but these errors were encountered: