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

Application domain/field

Type of tool

Deductive verifier

Expected input

Program annotated with specifications


Expected output

Whether the program adheres to the specification or not.


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.
C Concurrency Java


Related papers

Last publication date

17 October 2022

Related tools

ProVerB specific

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