PV1 ⊧ MetaValchecks whether the witness for a specific program and property is valid

Application domain/field

• Model checking
• Witnesses
• Witness validation

Type of tool

Witness validator (used in software model checking)

Expected input

• Program
• Specification
• Witness

Format:

• Program: C code
• Specification: SV-COMP format for specifications, .prp file
• Witness: SV-COMP format for witnesses (https://github.com/sosy-lab/sv-witnesses/)

Expected output

Per witness it reports whether it is confirmed (true/false) and the time it took to check it. It also presents a summary of statistics (number of correct, incorrect and unknown witnesses).

Internals

Uses CPAchecker.

Comments

A witness is a counterexample that can be used to observe a certain bug/error. This can be useful for debugging, generating tests, and more. A witness validator is used to verify that the witness is indeed a valid witness.