PV6 ⊧ IVydeductively or inductively proves or helps prove program properties

Application domain/field

• Protocol verification
• Distributed programs

Type of tool

Protocol verifier

Expected input

Program

Format:

.ivy file (program specified in the IVy language)

Expected output

Depends on the mode of operation:

1. ivy_check checks the proof of an IVy program, will return PASS or FAIL
2. ivy will allow the user to interactively construct inductive invariants
3. ivy_to_cpp will result in a C++ program extracted from the IVy program

Internals

Used for specifying, modeling, implementing and verifying protocols. "Tool for correct design and implementation of distributed protocols and algorithms, supporting modular specification, implementation and proof" Some things it can do:

• Checking safety/liveness via (1) deductive verification, (2) abstraction and model checking (3) manual proofs using natural deduction
• Compositional specification-based testing and bounded model checking
• Extract executable distributed programs by translation to efficient C++ code

Uses ABC, Z3.

Comments

License: MIT