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

Type of tool

Probabilistic model checker

Expected input


Expected output

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


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


License: Apache-2.0 license
Model checking Probabilistic


Repository: https://github.com/moves-rwth/kipro2

Related papers

Latticed k-Induction with an Application to Probabilistic Programs (CAV '21)

Last publication date

15 July 2021

ProVerB specific

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