LARA

This is an old revision of the document!


Verifying Programs with Global Containers

If instead of integers, our programs manipulate sets, the verification conditions will be in the set language and we can decide them by translation into exists-forall class.