How to verify loop with z3?

Question

I am a beginner user of Z3. How do I verify a loop (C code) with a loop invariant in Z3?

For ex:

int a[10],i;
for(i = 0; i<10; i++)
{    
  a[i] = 0;
}

See also https://stackoverflow.com/questions/48089983 – Malte Schwerhoff Jan 08 '18 at 07:41 — Malte Schwerhoff, Jan 08 '18 at 07:41

score 1 · Answer 1 · answered Jan 07 '18 at 02:34

Z3 only supports first-order logic with theories. You can use a program verification tool to map programs with assertions to logic. For example http://rise4fun.com/dafny or http://rise4fun.com/fstar. Reasonable courses on logic in computer science will also contain material on how to write a verification condition generator. These are better starting points for this question.

How to verify loop with z3?

1 Answers1