PV3 ⊧ Weaverchecks user-specified k-safety properties for programs in a simple imperative language

Given a program (in a simple imperative language), where a hyperproperty is encoded using an assume statement, it attempts to prove the property.

Application domain/field

• Hypersafety properties
• Reduction
• Counterexample-guided abstraction refinement (CEGAR)

Expected input

• Program
• Hyperproperty

Format:

• Program: simple imperative language
• Hyperproperty: encoded in the program with assume statements

Expected output

SUCCESS or FAILURE. In case of FAILURE it will also provide a counterexample.

Internals

Hypersafety property: A property that describes the set of valid interrelations between multiple finite runs of a program. k-safety property: safety property whose violation is witnessed by at least k finite runs of a program. Weaver reduces verification of k-safety properties to verification of 1-safety properties. As a result, it is then possible to use existing safety verification techniques. Uses Z3, MathSAT, Yices, CVC4.