PV4 ⊧ VerCorsverifies user-written properties and memory-safety for a program

Application domain/field

• Concurrency
• Deductive verification
• Auto-active verification

Type of tool

Deductive verifier

Expected input

Program annotated with specifications

Format:

• Program: C, Java, PVL (own language)
• Specifications: added as annotations (in comments) to the program, written in their own specification language that was inspired by JML.

Expected output

Whether the program adheres to the specification or not.

Internals

VerCors can be used to verify both functional properties and memory-safety. VerCors aims to verify concurrent and parallel programs. Two extensions have been built on top of VerCors namely Alpinist and VeyMont. Uses Viper.