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

Expected input


Expected output

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


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.


Repository: https://github.com/weaver-verifier/weaver

Related papers

Last publication date

12 July 2019

Related tools

Synonym: checks k-safety properties of Java programs

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.