Basic RAC for why3execute and CE validation
Add concrete and abstract runtime assertion checking (RAC) to the Why3 interpreter Pinterp
, and use it to derive validated counterexamples.
Add concrete and abstract runtime assertion checking (RAC) to the Why3 interpreter Pinterp
, and use it to derive validated counterexamples.