PV0 ⊧ EXIST

Application domain/field

• Probabilistic programs
• Invariant generation

Type of tool

Invariant inference tool

Expected input

• Number of runs
• Number of states
• Whether to learn a subinvariant or an exact invariant

Format:

Has to be passed as parameters to the Python program. If you want to run it on a different program/benchmark, then one should encode the program in their specific Python files.

Expected output

Invariants

Internals

Infers invariants for probabilistic programs. Exist will execute the program multiple times on a set of input states. It uses machine learning to learn models encoding possible invariants.