CODEWITHSUNDEEP
smtformal-verificationloop-invariant
desert_ranger
desert_ranger

Reputation: 1743

Does loop invariant verification using SMTs require enumerating values of variables?

I am trying to understand how loop invariant verification conditions work, particularly in the context of SMT solvers. Consider the following simple loop:

i = 0
while i < 10:
    i += 1

Suppose I incorrectly choose {i ≠ 7} as a loop invariant.

  1. This invariant holds at initialization (i = 0).
  2. However, during execution, there exists an iteration where i = 6, and after i += 1, we get i = 7, violating the invariant.

To catch this failure during verification, does an SMT solver need to enumerate possible values of i, or does it detect the violation symbolically? How exactly does it determine that {i ≠ 7} is not an invariant?

I would appreciate insights into how SMT solvers handle this kind of reasoning.

Upvotes: 0

Views: 23

Answers (1)

alias
alias

Reputation: 30525

This isn't something SMT solvers actually do. The so-called "Verification Conditions" will be setup by some other system, most likely a theorem-prover for the particular language you're working on. (Dafny, Why3, etc.) This system will then come up with a proof condition of the form:

 {i ≠ 7} {i = i + 1} {i ≠ 7}

It'll then translate this to the language of the SMT solver, likely in SMTLib, but possibly using the internal API. It'll most likely first put the statement into static single-assignment form, and then pose the problem to the solver. This'll necessarily look different for each tool, but it'll essentially say something like:

; Model i = i+1, create new variable and assert the equality
(declare-fun i  () Int)
(declare-fun i2 () Int)
(assert (= i2 (+ i 1)))

; Check the invariant is maintained by the loop
(assert (not (implies (distinct i 7) (distinct i2 7))))  

(check-sat)
(get-model)

Note that we assert the negation of what we want to prove, and hence the wrapping of not in the last assert. (This is the usual trick for SMT-solvers since they check for satisfiability. If negation is unsatisfiable, then we have a proof. If it is satisfiable, then we have a counter-example.)

For this, you get an output of the form:

sat
(
  (define-fun i () Int
    6)
  (define-fun i2 () Int
    7)
)

i.e., the solver tells you that i = 6 is a counter-example.

Note that the solver does not do this by enumeration. Instead it has a solver that can symbolically reason about such equations. How exactly it does that: there's a bunch of books/resources you can refer to. Start by looking at this answer: https://stackoverflow.com/a/70795825/936310

Upvotes: 1

Related Questions