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



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.


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.


Related papers

Last publication date


ProVerB specific

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