Re: "Verification Corner" videos, contract programming

[bearophile]

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