To do #7860

follow up in EUF summaries (Grisha's idea)

Added by Sepideh Asadi almost 6 years ago. Updated almost 6 years ago.

Start date:
Due date:
% Done:


Estimated time:


The point is about the loop in function func which calculates a new value for variable b. This loop is not needed for verifying any of assertions. It cannot be removed by slicing because variable b is used later in the program. But it can be identified by our summarization procedure.

So idea is to 1) skip the loop at all, and thus treat b nondeterministically, 2) solve the whole BMC formula with EUF and get the UNSAT result, 3) interpolate and analyze the EUF summary for func. If variable b does not appear in the summary, then we can safely remove the loop and trust the summary. If b appears in the summary, then the result is not trustable, and we go back to the encoding of main program with loop, (unroll the loop perhaps, lazily?) and re-check. If the result is SAT, then of course we also need to go back to the unrolling.

if you replace the assignment to b after the loop by nondet() and the formula is UNSAT, then you can trust the summary. But if you create an under-approximation of the loop (e.g., unroll it 1 / 2 / 5 / 10 times) and the formula is UNSAT then the summary is not trustable any more, and you may try the above trick.


#1 Updated by Sepideh Asadi almost 6 years ago

  • Assignee set to Sepideh Asadi

Also available in: Atom PDF