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

Automated deductive program verifier

Application domain/field

• Dynamic allocation
• Data structures
• Separation logic
• Functional correctness
• Heap manipulating programs
• Deductive verification

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:

• All procedures mutually satisfy their specified contracts
• All loops satisfy their loop invariants
• All heap accesses and memory deallocations are safe
• There are no memory leaks

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.