After a quick reminder of the Hoare Logic and the approach for designing software by contracts, the tool suite developed by AdaCore for formal verifications is presented. To make the concepts easily understood, a little program simulating a sandpile is used.
Speakers: Didier Willame