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

Format:

Internals

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
Java

Links

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

Last commit date

15 December 2018

Related papers

https://doi.org/10.1007/978-3-319-96145-3_9 (CAV '18)

Last publication date

18 July 2018

Related tools

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

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.