Proof of programs with Why3
Teacher: François Bobot
Different approaches to verification:
 model checking
 astract interpretation
 deductive verification (SAT solving)
Two kinds of verifications:

ensuring safety
 no false positive (when it says there’s no problem, you’re sure of it)

bug finding:
 e.g. on github: automatic bug finding
Sucess stories:

metro in Paris: line A is nowadays completely automatic. At the beginning, the programming was handmade, but it was very buggy. But today: uses refinement ⟶ automatically verified

Astrée project (used for flight control)

Compcert: certified C complier (with Coq)
 this compiler is not as good as
gcc
is 0.3, but definitely better than it in earlier versions ⟶ used by Airbus nowadays
 this compiler is not as good as
 EDF (in France) use FramaC Eva, Airbus use FramaC WP, etc…
 Airbus is already ensuring that their code is bugfree (because it’s really critical), but verification tools help to check everything automatically, which curb costs
 Spark2014: verifies a subset of Ada programs
Hoare logic
Will be replaced at the end of the course by something more modern
Expressions
e ::= n (integer constants)
 x (variables)
 e op e
Integers, variables, binary operations
op ::= +  −  ∗
 =  ≠  <  >  ≤  ≥
 and  or
 Statements:

s ::= skip (no effect)  x := e (assignment)  s ; s (sequence)  if e then s else s (conditional)  while e do s (loop)
Example of a program computing the square root:
count := 0; sum := 1;
while sum ≤ n do
count := count + 1; sum := sum + 2 * count + 1
To express formal properties: firstorder logic
\[p ::= e \; \mid \; p ∧ p \; \mid \; p ∨ p \; \mid \; ¬p \; \mid \; p ⇒ p \; \mid \; ∀v, p \; \mid \; ∃v, p\] Hoare triples:

Precondition followed by a program
s
and a postcondition: \(\{P\}s\{Q\}\)
Examples:
{x = 1}x := x + 2{x = 3}
{x = y}x := x + y{x = 2 ∗ y}
{true}while 1 do skip{false}
or for the square root (actually: integer part of $\sqrt{n}$) program:
{n ≥ 0}ISQRT{count² ≤ n ∧ n < (count + 1)²}
\[\cfrac{}{\{P[x ⟻ e]\} x:=e \{P\}}\]
or
\[\cfrac{}{\{P\} x:=e \{∃ v \; P[x ⟻ v]\}}\]Often, the postcondition gives you a hint as to what the invariant of a loop should be.
\[\infer{\{P\} x := e \{∃v; e[x ← v] = x ∧ P[x ← v]\}}{ \infer{\vdots }{ \infer{\{P[x ← e]\} x:=e \{P\}}{\phantom{\{P[x ← e]\} x:=e \{P\}}} } }\]
assume
⟹ assert
 Frame property:

if you have $\lbrace P \rbrace C \lbrace Q \rbrace$ and $R$ is a property not modified by $C$, then you have $\lbrace P ∧ R \rbrace C \lbrace Q ∧ R \rbrace$
Leave a comment