afm09-why-tutorial

Why—an intermediate languagefor deductive program verificationJean-Christophe FilliˆatreCNRSOrsay, FranceAFM workshopGrenoble, June 27, 2009Jean-Christophe Filliˆatre Why tutorial AFM’09 1 / 56Motivationshow to do deductive program verification on realistic programs?deductive verification means that we want to prove safety but alsobehavioral correctness, with arbitrary proof complexityrealistic programs means pointers, aliases, dynamic allocation,arbitrary data structures, etc.Jean-Christophe Filliˆatre Why tutorial AFM’09 2 / 56Motivationssince Hoare logic (1968), we know how to turn a program correctnessinto logical formulas, the so-called verification conditionswe coulddesign Hoare logic rules for a real programming languagechoose an interactive theorem proverthe Why approach: don’t do that!Jean-Christophe Filliˆatre Why tutorial AFM’09 3 / 56Principlesinstead,design a small language dedicated to program verificationand compile complex programs into ituse as many theorem provers as possible (interactive or automatic)Jean-Christophe Filliˆatre Why tutorial AFM’09 4 / 56Related Workthere is another such tool: the Boogie tool developed at MicrosoftResearch, initially in the context of the SPEC# project (Barnett, Leino,Schulte)there are differences but the main idea is the same: verification conditionsshould be computed on a small, dedicated languageJean-Christophe Filliˆatre Why tutorial AFM’09 5 / 56Overview1 theWhy languageand its ...