VCC is sound ?

Oct 14, 2011 at 2:18 PM

I am so interested in VCC,on the home page I know VCC is sound.

If we want to prove VCC is sound ,the VCC must have operational semantics and axiomatic semantics,but I can't find these in the documentation and publications .

Could anybody show me the detailed operational and axiomatic semantics or the link?

Thanks a lot.

Oct 20, 2011 at 12:32 PM

The soundness of invariant admissibility, ownership, and claims is described in the CAV paper.

The 2009 tech report gives the operational semantics of a small language, and describes the reduction theorem that allows us to pretend that scheduler boundaries occur only before atomic actions (with a suitable interpretation of what assertions within threads mean).

The semantics we use for sequential C is essentially given in the translation to Boogie, which you can find in the source code but has not been written about separately.

Sabine Schmaltz <> is working on a more careful operational semantics and soundness proof; you might want to contact her directly.