search

LKlinke / Prodigy

A tool that analyses probabilistic programs, allows for automatic invariance checking and handles inference all based on Generatingfunctionology.
Apache License 2.0
2 stars 0 forks source link

CTI Usage #16

Open LKlinke opened 1 year ago

LKlinke commented 1 year ago

When doing the equivalence check and seeing that Loop and invariant are not equivalent, make use of the generated counterexamples to induction to refine the invariant template.