PV3 ⊧ KIPRO2 (sometimes stylized as kipro2)checks properties of a pCGL program

KIPRO2: k-Induction for probabilistic programs (note: 2 is part of the name, not a version number)

Application domain/field

• Model checking
• Bounded model checking (BMC)
• k-induction
• Probabilistic programs

Type of tool

Probabilistic model checker

Expected input

• pGCL program
• Pre-/post-expectations
• Checker to use: kind/bmc/both (i.e. k-induction, bounded model checking, or both)

Format:

• pGCL program: .pgcl file
• Pre-/post-expectations: parameters when executing the tool, or as comment in the model ("// ARGS: --post [arg] --pre [arg] ")
• Checker: parameter when executing the tool, or as a comment in the model ("// ARGS: --checker [arg]")

Expected output

Whether the property could be proven, if not then a counterexample is provided.

Internals

It performs in parallel latticed k-induction and BMC (bounded model checking) to fully automatically verify upper bounds on expected values of {pGCL} programs. It can also reason about expected values, e.g. expected runtimes, of such programs. Uses Z3, PySMT

Comments

License: Apache-2.0 license