Brussels / 1 & 2 February 2014


Formal Verification with Ada 2012: a Very Simple Case Study

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.


Didier Willame