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

Prototype for verifying k-safety properties of Java programs

Application domain/field

• Relational verification
• Relational specifications
• Safety verification

Type of tool

Relational verifier

Expected input

• Program
• Reference to property that should be verified
• Tool that should be used for verification

Format:

• Program: Java file
• Property to be verified: a number that is passed as an argument. The number indicates which property from Properties.hs to check
• Tool for verification: passed as an argument: descartes, syn, or synonym

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