"Verification Corner" videos, contract programming

[deadalnix]

Le 12/06/2012 14:55, bearophile a écrit :
> deadalnix:
>
>> I wonder what is the method used by the compiler to ensure most of the
>> check at compile time.
>
> It uses Z3 and Boogie:
> http://rise4fun.com/
>
> Bye,
> bearophile

OK, but how does that work internally :D Some example are 
straightforward, but others are really black magic to me.