PV3 Synonymchecks user-specified k-safety properties for Java programs

Prototype for verifying k-safety properties of Java programs

Application domain/field

Type of tool

Relational verifier

Expected input



Relational specifications: Specifications that can describe multiple runs of the same program or relate the behaviors of multiple programs. k-safety properties are relational verification problems over k identical Java programs. Built on top of Descartes


Repository: https://github.com/lmpick/synonym

Related papers

Exploiting Synchrony and Symmetry in Relational Verification (CAV '18)

Last publication date

18 July 2018

Related tools

Tools for relational verification: Rosette/Unbound, VeriMapRel, Reve, MoCHi, SymDiff

ProVerB specific

Markdown description: view/edit

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