CEGIS

Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants
Essential tasks for the verification of probabilistic programs include bounding expected outcomes and proving termination in finite …
PDF Cite DOI Artifact Evaluated
Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants
NIL: Learning Nonlinear Interpolants
Nonlinear interpolants have been shown useful for the verification of programs and hybrid systems in contexts of theorem proving, model …
PDF Cite Code Slides DOI
NIL: Learning Nonlinear Interpolants