sv-witnesses
sv-witnesses copied to clipboard
sosy-lab
An Exchange Format for Verification Witnesses (MOVED, please follow the link)
This depends on #61 being merged, the PR diff currently isn't nice, but a nicer diff can be seen here: https://github.com/sim642/sv-witnesses/compare/yaml-schema...goblint:sv-witnesses:flow_insensitive_invariant. While loop invariants and location invariants (#62) are associated...
This adapts #59 on top of #61. Since this depends on #61 being merged, the PR diff currently isn't nice, but a nicer diff can be seen here: https://github.com/sim642/sv-witnesses/compare/yaml-schema...goblint:sv-witnesses:location_invariant. ###...
### Changes 1. Replace `loop_invariant` schema with a combined schema that also specifies `loop_invariant_certificate`. 2. Add descriptions to schema. 3. Extract reusable `$defs` in schema to simplify new entry type...
This PR introduces a new entry type for YAML-based witnesses that describes location invariants.
In a discussion between some Munich Goblint folks and @MartinSpiessl and others from the CPAChecker team on Friday we were wondering whether `loop_invariant` is actually the right name for the...
This PR intends to address #27. I have never distributed a package before, so feedback is welcome.
Last year there were several threading-related issues with the linter which raised questions about the witness specification (cf. #30, #33, #36). This PR is to fix the handling of threading-related...
For people who are users of the GraphML format the instructions on how to configure CPAchecker to do a witness validation with a non-standard analysis should not be listed here....
This PR is based on #33 and improves the documentation about the usage of thread identifiers. It also disables the current check for thread creation.
With the previous specification, the initially active thread (as created by starting a program) could not be referenced in transitions without violating the specification (only threads specified in createThread could...
