Verify programs with Contracts

Different kinds of contracts

CIVL generally provides three kinds of contracts:

• Contracts for sequential programs
• Contracts for MPI
• Contracts for reduction (see ContractReduction)

All these contracts in CIVL are developed as extensions on ACSL language.

Contracts for sequential programs

Contracts for sequential programs are based on the theory of Hoare Logic. Contracts only state sequential properties on either 
the pre-state or post-state of the given procedure. All sequential contract constructors are inherited from ACLS, CIVL will start 
from supporting part of them.

Contracts for MPI programs

Contracts for MPI programs are contracts stating specific properties of MPI programs. MPI contracts must be introduced by an MPI behavior constructor. To be consistent with