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

Format:

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

Links

Related papers

Last publication date

17 October 2022

Related tools

ProVerB specific



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