Skip to content
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

Reject YAML violation witnesses #1301

Closed
sim642 opened this issue Dec 19, 2023 · 1 comment · Fixed by #1512
Closed

Reject YAML violation witnesses #1301

sim642 opened this issue Dec 19, 2023 · 1 comment · Fixed by #1512
Assignees
Labels
feature sv-comp SV-COMP (analyses, results), witnesses
Milestone

Comments

@sim642
Copy link
Member

sim642 commented Dec 19, 2023

We can reject violation witnesses for programs that we can prove correct, assuming we are sound. This probably won't make us very good in the validation track though.

We could also consider actually interpreting the YAML violation witness and refining our analysis with that information. If there's no violation in the state space restricted by the violation witness and we can prove it, the witness is also invalid.

@sim642
Copy link
Member Author

sim642 commented Jun 20, 2024

I guess we could also reject GraphML violation witnesses based on verdict, but it's probably kind of pointless. GraphML witnesses might become unused in SV-COMP sometime anyway.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
feature sv-comp SV-COMP (analyses, results), witnesses
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant