PV4 GRASShopperchecks user-specified contracts and memory safety of programs in its own language

Automated deductive program verifier

Application domain/field

Type of tool

Deductive verifier

Expected input

Program

Format:

Own simple procedural imperative language that supports user-defined struct types and arrays. (.spl file)

Expected output

It will indicate errors in the program or specification.

Internals

Given an input program, GRASShopper will check the following: GRASShopper focuses on a decidable specification logic so that the proof obligations can be reduced to a decidable fragment of first-order logic. Uses Z3, CVC4.

Links

Related papers

Last publication date

2014

ProVerB specific



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