[YICES-HELP] Using SMT to Model Check C

[Bruno Dutertre]

Tom Hawkins wrote:
> I would like to use Yices to model check some embedded C code.  I have
> a basic understanding of how SMT is applied to BMC and k-induction for
> systems with a single transition relation, but how can it be used for
> imperative programs, or more specifically, control flow graphs with
> conditional branches and loops (i.e. all functions inlined, assuming
> no recursive functions)?
> 
> The following example could be a prime candidate for BMC...
> 
> void main() {
>   ...
>   while (...) {
>     ...
>     assert(...);
>   }
> }
> 
> But what should be done when assertions are outside of loops...
> 
> void main () {
>   ...
>   while (...) doSomething();
>   while (...) doSomethingElse();
>   assert(...);
> }
> 
> ... or when an assertion is placed in a loop, outside of another, with
> a mix of conditional branches?
> 
> One thought I had was to transform the control flow graph into an
> abstract machine, with state elements and a program counter, then
> define the transition relation as how the machine changes state
> executing a single statement or instruction.  This way, conventional
> BMC could be applied, but I suspect it would add a lot of complexity
> to the model.
> 
> Any thoughts or suggestions?  Can anyone recommend any research papers
> that apply SAT/SMT model checking to imperative programs?
> 
> Thanks!
> 
> -Tom
> 

I'm not an expert, but I'd assume bounded model checking of code
requires that you enroll the loops finitely many times.

Bruno