search

gradual-verification / silicon-gv

Mozilla Public License 2.0
0 stars 3 forks source link

Explore checkSmoke paths through static verification (aka. infeasible paths) #18

Open jennalwise opened 2 years ago

jennalwise commented 2 years ago

Now that I understand the purpose of checkSmoke, which is to ensure that the verifier is going down an infeasible path (one that could be created by an unsat symbolic state, I think if I remember correctly), I need to go back and make sure the uses of it are consistent with semantics expected of the gradual static verifier.

jennalwise commented 2 years ago

methods.vpr might be helpful in debugging/exploring this.

jennalwise commented 2 years ago

This should not affect the validity of the OOPLSA'22 results as those examples should not execute down an infeasible path.