Introduction

Contexte

PB : Comment vérifier qu’un logiciel fonctionne ?

Pourquoi :

• Conséquences :
  • Financières
  • Vies humaines
  • Résilience aux attaques (sécurité)
  • Conformité avec la loi
  • Utilisateurs peuvent en avoir besoin (frustration)

Comment :

• Revue de code
• Tests

Exemple de bugs connus : …

On a aussi utilisé des méthodes “informelles”. Ça passe mal à l’échelle.

Et les méthodes 100% automatiques n’existent pas (indécidabilité de Riesz).

Il y a donc différents niveaux d’automatisation :

(F* : types incluent logique d’ordre 1)

Dans ce cours

• Logique de programme
• Preuve automatique de formules via SMTSolver

Objectifs

• Comprendre les fondements de cette approche
• Comprendre en programmant (projet)

Format

Cours

• Normal : 3h / semaine, ou 1h30 si pas le temps
• Février : Alexandre Drewery 1h30

CM / TD / TP mélangés

Évaluation

• Devoir sur table pour évaluer la bonne compréhension du cours
• Show & Tell : 20 min de présentation (preuve / algo) + 10 min présentation
• 1 ou 2 projets de prog par groupe de 2 ou 3

Biblio

• Decision procedures
• Kroning

Séance 1 : Logique de programme

Prouver qu’un programme est correct nécessite de spécifier ce que correct signifie.

Exemple :

s = 0
k = 0
while k < N:
    s += k
    k += 1

Que fait ce programme ? Il calcule la somme des N - 1 premiers entiers : 0 + ... + (N - 1) = N (N - 1).

SI N \geq 0 !

Il faut faire attention aux préconditions…

Ici, on va utiliser plusieurs outils.

Notation de Hoare

Informellement, \left< P \right> c \left< Q \right> signifie :

Si on exécute le programme c en partant d’un état initial vérifiant l’état P, alors la post condition Q est vérifiée à la fin de l’exécution, si c termine.

RQ : Il s’agit de correction partielle : ça fonctionne si c termine.

On peut aussi utiliser un critère plus fort de correction totale :

[P] c [Q] signifie la même chose, avec la garantie en plus que c termine sur l’exécution à partir d’état initiaux satisfaisant P.

Exemples :

• Programme permutant x et y :

# x & y des references
def swap(x,y):
    z = x
    x = y
    y = z

Triplet de hoare correspondant :

\left<x = a \land y = b \right> swap \left< x = b \land y = a \right>

Avec a et b des variables “fantômes” non libre dans la commande.

• Programme de tri :
  \left< T = T_0 \right> sort(T) \left< trié(T,N) \land permutation(T,T_0,N) \right>
  Avec : permutation(T, T', N) := len(T) = len(T') \land \forall i \in [0, N[, \exists j \in [0, N[, T_i = T'_j
  et : trié(T) := \forall i \in [0, N[, T_i \leq T_{i+1}

Syntaxe

Un mini langage impératif

c ::= skip
| x := t
| c1; c2
| if t then c1 else c2
| while t do c

On dit que t est un terme, par exemple : x y z 1 3.14 -x -(x+1) sin(x)

Les assertions

• pré, post, …, invariant
• On se restreint à la logique d’ordre 1

Rappels de logique

• Notion de terme (arbre n-aire avec des variables aux feuilles)
• Notion d’atome :
  • \top (vrai)
  • \bot (faux)
• Notion de formule :

F ::= <atome>
| not F
| F1 and F2
| F1 or F2
| F1 => F2
| F1 <=> F2
| exists x. F
| forall x. F

Exercice :

Si, \left< P1 \right> c \left< Q1 \right> et \left< P2 \right> c \left< Q2 \right>, Peut on affirmer :

• \left< P1 \land P2 \right> c \left< Q1 \land Q2 \right> ?
• \left< P1 \lor P2 \right> c \left< Q1 \lor Q2 \right> ?

Correction : Les deux sont vraies.

Séance 2 : Logique de Hoare, formalisée

Triplets de Hoare

Programmes annotés

Pour éviter d’avoir à écrire des triplets \left< P \right> c \left< Q \right>, et les arbres de dérivations correspondant, on va annoter les programmes avec des assertion intermédiaires.

Exemple :

<y = a> => <I[0/x]>
x := 0
<I>
while y > 0 do
    <I /\ y > 0> => <I[(x+1)/x][(y+1)/y]>
    y := y - 1
    <I[(x+1)/x]>
    x := x + 1
    <I>
<I /\ not y > 0> => <x = a \/ a < 0>

On va définir la syntaxe suivante pour ces programmes “augmentés” :

d ::= skip<Q>
| x := e<Q>
| d; d
| if b do <P1> c1 else <P2> c2 <Q>
| while b do <P> c <Q>
| => <P> d
| d => <Q>

dc ::= <P> d

On définit par ailleurs les 3 fonctions eff, pre et post suivantes, définit inductivement :

eff(<P> d) = eff(d)
eff(skip <Q>) = skip
eff(x := e <Q>) = x := e
eff(while b do <P> c Q) := while b do eff(c)


pre(<P> d) = P

post(<P> d) = post(d)
post(skip <Q>) = Q
post(while b do <P> c <Q>) = Q
post(c1; c2) = post(c2)

L’intuition est que \left< P \right> d est valide ssi \left< P \right> \text{eff}(d) \left< \text{post}(Q) \right>.

RQ : Ce système est totalement dirigé par la syntaxe <3

Mais : Correction, completude… ?

Correction et complètude des programmes annotés dans la logique de Hoare

Preuve :

On procède par induction sur d.

On note \mathbf{P}(d) := \forall P, \left< P \right> d \implies \left< P \right> \text{ eff}(d) \left< \text{ post}(d) \right>

Principe d’induction :

Si :

• \forall Q, \mathbf{P}(\text{skip} \left< Q \right>)
• \forall x,e,Q, \mathbf{P}(x:=e \left< Q \right>)
• \forall d_1, d_2, \mathbf{P}(d_1) \land \mathbf{d_2} \implies \mathbf{P}(d_1; d_2)
• …

Alors \forall d, \mathbf{P}(d).

Retour à la preuve :

On traite uniquement le cas ‘skip’ ici :

Soit d_1, d_2, supposons que \mathbf{P}(d_1) et \mathbf{P}(d_2).

Soit P tq P \vdash d_1;d2.

Montrons que \left< P \right> \text{eff}(d_1);\text{eff}(d_2) \left< \text{post}(d_2) \right>

1. Si P \vdash d_1 alors \left< P \right> \text{eff}(d_1) \left< \text{post}(d_1) \right>
2. Si \text{post}(d_1) \vdash d_1 alors \left< \text{post}(d_1) \right> \text{eff}(d_2) \left< \text{post}(d_2) \right>
3. Si P \vdash d_1 et \text{post}(d_1) \vdash d_2 : par 1) + 2), on conclut avec la règle de la séquence de \cdot \vdash \cdot.

On fait la preuve par induction sur \left< P \right> c \left< Q \right>.

Principe d’induction :

Si :

1. \forall A, \mathbf{P}(A,\text{skip},A)
4. …
5. \forall I, b, c, si \mathbf{P}(I \land b,c,I) alors \mathbf{P}(I, \text{while } b \text{ do } c, I \land \lnot b).
6. \forall P, P', Q, Q', c, si \models P \implies P' \land \models Q' \implies Q \land \mathbf{P}(P',c,Q'), alors \mathbf{P}(P, c, Q)

Alors : \forall P, c, Q, \left< P \right> c \left< Q \right> \implies \mathbf{P}(P,c,Q).

Retour à la preuve (uniquement le cas 5) :

5. Appelons d' tq c=\text{while } b \text{ do } c'

   1. \text{eff}(d') = c'
   2. \text{post}(d') = I
   3. I \land b \vdash d'

   Considérons d = \text{while } b \text{ do } \left< I \land b \right> d' \left< I \land \lnot b' \right>. Il vérifie :

   1. \text{eff}(d) = \text{while } b \text{ do } \text{eff}(d') = c
   2. \text{post}(d) = I \land \lnot b
   3. I \vdash d d’après la règle du while

Exo : Annoter le programme suivant de sorte à ce qu’il soit valide :

<y >= 0>

p := 0

k := 1

while k <= y do

    p := p+x

    k := k + 1
done

<p = x*y>

Correction :

<y >= 0>
=> <I[1/k]> *
p := 0
k := 1
<I:= p = (k-1)*x /\ k <= y+1>
while k <= y do
    <I and k <= y>
    => <I[(k+1)/k][(p+x)/p]> **
    p := p+x
    <I[(k+1)/k]>
    k := k + 1
    <I>
done
<I /\ not k <= y>
=> <p = x*y> ***

* : \models y \geq 0 \implies 0 = (1-1)w \land 1 \leq y + 1 \square

** : \models I \land k \leq y \implies p+x=((k+1)-1)x \land k+1 \leq y + 1 \square

*** : I \land \lnot k \leq y \implies p = k x \square

Séance 3 : Obligations de preuves

\rightarrow Repartons de la logique IMP, en modifiant la structure du while.

c ::= ... | <I> while b do c

et la règle associée devient :

\left< I \land b \right> c \left< I \right> \rightarrow \left< I \right> \text{while } b \text{ do } c \left< \left< I \right> I \land \lnot b \right>

Construisons maintenant une formule PO(P,c,Q) telle que : \models PO(P,c,Q) \iff \left< P \right> c \left< Q \right>

Calculons d’abors la “meilleure” précondition pour c et Q donné :

• pre(\text{skip}, Q) = Q
• pre(\text{x:=e}, Q) = Q[\frac{e}{x}]
• pre(c_1;c_2, Q) = pre(c_1, pre(c_2, Q))
• pre(\text{if } b \text{ then } c_1 \text{ else } c_2, Q) = (b \implies pre(c_1, Q)) \land (\lnot b \implies pre(c_2, Q))
• pre(\left< I \right> \text{ while } b \text{ do } c, Q) = I

VC (Verification Condition) :

• VC(\text{skip}, Q) = VC(\text{x:=e}, Q) = \top
• VC(c_1;c_2, Q) = VC(c_2, Q) \land VC(c_1, pre(c_2,Q))
• pre(\text{if } b \text{ then } c_1 \text{ else } c_2, Q) = VC(c_1, Q) \land VC(c_2, Q)
• VC(\left< I \right> \text{ while } b \text{ do } c, Q) = VC(c, I) \land (I \land b \implies pre(c, I) \land (I \land \lnot b \implies Q))

Ce qui nous donne :

PO(P, c, Q = P \implies pre(c,Q) \land VC(c,Q)

Preuve :

On procède par induction sur c :

• Cas c = x := e
  Alors pre(c,Q) = Q[\frac{e}{x}] donc \left< prec(c,Q) \right> c \left< Q \right>

• Cas c = \left< I \right> \text{ while } b \text{ do } c' :
  Alors pre(c,Q) = I. Mq \left< I \right> c \left< Q \right> :

  |= I /\ b => pre(c', I) (a)   <pre(c', I)> c' <I> (b)
  -----------------------------------------------------
  <I /\ b> c' <I>
  ------------------------------------------------------------
  <I> <I> while b do b' <I /\ not b>    |= I /\ not b => Q (c)
  ------------------------------------------------------------
  <I> <I> while b do c' <Q>

  1. : vrai par def de VC
  2. : Il suffit de prouver \models VC(c',I) par hypothèse d’induction. C’est vrai par def de VC.
  3. : vrai par def de VC

On le prouve à l’aide de 2 lemmes intermédiaires :

Preuve par induction sur \left< P \right> c \left< Q \right> :

• Cas 1 : c = \text{skip}, P = Q.
  Donc pre(c,Q) = P, donc il suffit \models P \implies P, ce qui est vrai
• Cas 2 : c = c_1;c_2.

  • \left< A \right> c_1 \left< B \right> donc \models A \implies pre(c_1, B) par HI.

  • \left< B \right> c_2 \left< C \right> donc \models B \implies pre(c_2, C) par HI.

    Monotonie de pre

    Pour tout c, Q_1, Q_2, si \models Q_1 \implies Q_2, alors \models pre(c, Q_1) \implies pre(c, Q_2).

    Comme on a \models A \implies pre(c_1, pre(c_2, Q) et \models pre(c_1, B) \implies pre(c_1, pre(c_2, C)) par def, d’après le lemme précédent, \models A \implies pre(c_1;c_2, Q).

    Ce lemme quant à lui se montre par induction sur c :

    • Cas c = c_1;c_2 :

      • H_1 : \forall Q_1, Q_2, \models Q_1 \implies Q_2 alors \models pre(c_1, Q_1) \implies pre(c_2, Q_2)
      • H_2 : \forall Q_1, Q_2, \models Q_1 \implies Q_2 alors \models pre(c_1, Q_1) \implies pre(c_2, Q_2)

      D’après H_2, \models pre(c_2, Q_1) \implies pre(c_2, Q_2), et d’après H_1, \models pre(c_1, pre(c_2, Q_1)) \implies pre(c_1, pre(c_2, Q_2)).

    • Cas c = \text{x := e} : \forall Q_1, Q_2, si \models Q_1 \implies Q_2 alors \models Q_1[\frac{e}{x}] \implies Q_2[\frac{e}{x}].

      Or, (lemme dont la preuve est laissée au lecteur) :

      M, I \models F[\frac{e}{x}] \iff M,I[x \mapsto I(e)] \models F

      Donc pour tout M :

      • \forall I, M, I \models Q_1 \implies Q_2
      • \forall I, M, I[x \mapsto I(e)] \models Q_1 \implies Q_2
      • Donc \forall I, M, I \models Q_1[] \implies Q_2[]

      Donc \models Q_1[] \implies Q_2[]

• …

Encore une fois, on procède par induction sur \left< P \right> c \left< Q \right> :

• Cas c = \left< I \right> \text{while } b \text{ do } c :
  On a P = I, Q = I \land \lnot b.

  TODO \models VC(c', I) \left< I \land b \right> c' \left< I \right>.

  Il faut prouver :

  • \models VC(c', I) : C’est bon.
  • \models I \land b \implies pre(c', I) : D’après la complétude 1.
  • \models I \land \lnot b \implies Q : Il faut encore un autre lemme de monotonie, et après c’est bon.

Séance 4 : Solveurs SMT

Notations

(CF cours de logique aussi).

T \models F signifie, F est valide (universellement) dans la théorie T.

On appelle théorie des axiomes (sous forme close), et une signature (symboles de fonctions et de prédicats).

La théorie vide n’a pas d’axiomes, et une infinité de symboles.

Solveurs SAT

Cependant, les solveurs SAT résolvent des pb à en gros 100 variables et 1000 clauses en quelques minutes.

Naivement, on pourrait essayer de faire du brute force avec une table de vérité… Mais c’est mauvais même en pratique.

DPLL

Il s’agit de l’algorithme de Davis–Putnam–Logemann–Loveland. Il procède par backtracking et usage d’heuristiques.

Fonctionnement

On se donne un état, consistant en une pile de couples (littéral, statut décidé / propagé) (on peut le voir comme un modèle partiel).

À chaque étape, l’algorithme va assigner une valeur au littéral courant, simplifier la formule et vérifier si elle est satisfiable. Si c’est le cas, il renvoit vrai, sinon, il backtrack, jusqu’à avoir parcouru l’ensemble des possibles.

Par rapport à un backtracking classique, DPLL va appliquer à chaque étape les actions suivantes de sorte à optimiser les performances :

• Unit Propagation : Si une clause est unitaire, on lui assigne la valeur nécessaire pour qu’elle soit vraie, et on la supprime de la formule. De la sorte, on simplifie grandement la formule.
• Pure literral elimination : Si un littéral est pur (e.g. apparait uniquement sous la forme x ou \lnot x, mais pas les deux à la fois), on peut faire en sorte de le mettre à vrai, et ainsi simplifier la formule.

On peut le formaliser de la manière suivante sous forme de transitions avec la pile :

1. Décide : M \rightarrow M l^D si l \not \in M \land \lnot l \not \in M
2. Prop Unitaire (l) : M \rightarrow M l si : \exists C \lor l \in F, M \models \lnot C \land l \not \in M \land \lnot l \not \in M.
3. Backtrack : M l^D N \rightarrow M \lnot l si \exists C \in F, M l^D N \models \lnot C, et N n’a pas de littéraux de décision.
4. Fail : M \rightarrow UNSAT, si M n’a pas de décision et M \models \lnot F
5. Success : M \rightarrow SAT si M \models F

Avec la notation : l^D signifie : on est en train de décider le littéral l.

RQ : Il reste un partie difficile… C’est de faire 2) efficacement.

CDCL (Conflict Driven Clause Learning)

Cet algorithme est souvent plus efficace dans l’ellagage que DPLL.

Il se base sur le même principe que DPLL, mais par rapport à ce dernier :

• On remplace la règle de backtracking par une nouvelle règle de back jumping.
• On modifie parfois F en lui ajoutant une clause de conflit.

Ce qui nous donne :

1. Décide (l) : M, F \rightarrow M l^D, F si …
2. …
3. Backjumping (C, l') : M l^D N, F \rightarrow M l', F \land (C \lor l') si F \models C \lor l' et M \models \lnot C.
4. …
5. …

RQ 1 : Truc difficile : Comment choisir C ? CF cours logique L3.

RQ 2 : On peut séparer la règle de Backjump en 2 :

• Learn (C) : (M, F) \rightarrow (M, F \land C) si F \models C.
• Backjump (C, l') : (M_1 l^D M_2, F) \rightarrow (M_1 l', F) si F \models \lnot C et C \lor l' \in F et l' indéfini dans M_1.

Exemple d’application :

\begin{aligned} F &= (c_1 := a \lor b)\\ &\land (c_2 := a \lor \lnot b)\\ &\land (c_3 := \lnot a \lor c \lor d)\\ &\land (c_4 := \lnot a \lor c \lor \lnot d)\\ &\land (c_5 := \lnot a \lor \lnot c \lor d)\\ &\land (c_6 := \lnot a \land \lnot c \lor \lnot d)\\ &\end{aligned}

FOL (First Order Logic) sans quantificateurs ?

Solveur de théorie : pour répondre au pb, \left< F | T \models F \right>

Notation : / Q : Quantifiée. / QF : pas quantifiée.

* : 3 axiomes :

• \forall a, i, j, i = j \implies \text{get}(a,i) = \text{get}(a,j)
• \forall a, i, j, v, i = j \implies \text{get}(\text{store}(a,i,v), j) = v
• \forall a, i, j, v, i \not = j \implies \text{get}(\text{store}(a,i,v), j) = \text{get}(a,j)

Combiner solveur SAT et solveur de théories ?

On se base sur des formules CNF : il existe une transformation linéaire (de Tseitin) qui transforme une formule F en une formule CNF F_{CNF} qui lui est équisatisfiable.

Combinaison EAGER

• Modifie chaque atome par un variable propositionelle ABSTRACTION ()
• Énumère tout les modèles booléens de \alpha(F)

Exemple :

\begin{aligned} F &= (P := g(a) = c)\\ &\land ((\lnot Q := f(g(a))) \neq f(c)) \lor (M := g(a = d))\\ &\land (\lnot S := c \neq d) \end{aligned}

On utilise une abstraction booléenne :

• \alpha (g(a) = c) =: p
• \alpha (f(g(a)) = f(c)) =: q
• \alpha (g(a) = d) =: r
• \alpha (c = d) =: s

D’où : \alpha(F) := p \land q \land (\lnot q \lor r) \land \lnot s

On ajoute alors les contraintes encodant (partiellemen) les axiomes de la théorie (ici EUF) :

• H_1 := p \implies q
• H_2 := p \land r \implies s

Et on donne au solveur SAT : H_1 \land H_2 \land \alpha(F), qui prouve UNSAT.

Combinaison LAZY

On conserve l’idée d’abstraction booléenne \alpha, mais on va chercher à avoir une interaction plus fine.

Lazy “simple”

On introduit la transformation inverse de \alpha, \gamma (aussi appelée concrétisation).

• Examine tout les modèles booléens M de \alpha (F).
• Vérifie si pour chaque décision \gamma (M) est unsat dans \top.

Exemple : On reprend celui de la combinaison eager.

M_1 := p \land \lnot q \land \lnot r \land \lnot s

\gamma (M_1) := g(a) = c \land f(g(a)) \neq f(c) \land g(a) \neq d \land c \neq d

Mais un SAT solveur ne donne en général qu’un modèle booléen dans le cas SAT. Pour le forcer à tout donner, on peut :

Si il nous donne un modèle M, ajouter \lnot M à la formule, et recommencer jusqu’à UNSAT.

DPLL (T) e.g DPLL modulo Théorie

RQ : On peut aussi (évidemment) utiliser CDCL.

On crée une boucle d’instanciation entre DPLL et le solveur de théorie.

RQ : Ce tableau ce lit de gauche à droite, de bas en haut. On peut voir ça de la manière suivante :

• La colonne DPLL trouve des modèles, et envoie ses infos à la colonne EUF sur la même ligne.
• La colonne EUF trouve des modèles, et envoie ses infos à la colonne DPLL de la ligne en dessous.

Et cela jusqu’à ce que DPLL soit UNSAT.

Plus précisément :

• Le solveur SAT travaille sur M et \alpha(F).
• Le solveur de théorie travaille sur \gamma(M)

Cela nous donne les règles suivante pour notre algorithme :

Exemple (on reprend la formule F) :

Trace de \text{DPLL}(T) :

RQ : Les règles de Backjump et Fail n’ont pas besoin de T-solveur, car on sait déjà : M \models \lnot C.

Le T-solveur n’est utilise que T-propagate et T-conflict.

Reprenons par ailleurs l’exemple, sans T-propagate pour montrer l’optimisation qu’elle apporte.

RQ : On ne peut cependant pas se passer de T-conflict.

Conclusion

• Que demande t on à un SMT solveur : \exists a', \land_i a_i \models a' ?
• \land_i a_i \models \bot ?
• Solveurs incrémentaux (passer d’un candidat de solution à un autre est peu coûteux) ?

Séance 5 : Théorie de l’égalité

On a vu que dans un SMT solveur, on s’intéressait à combiner un SAT solveur avec un solveur de théorie.

Aujourd’hui, on va s’intéresser à une théorie particulière, la théorie EUF (Equality + Uninterpreted Functions).

Théorie EUF

Exemple de formules : \forall x,y, f(x) = g(y) \implies g(x) = f(y)

Ici, on se restreint à QFEUF (Quantifier Free EUF).

Procédure de décision pour SAT QFEUF

Idée : On recherche la cloture par congruence de égalités du monome c’est à dire la plus petite relation de congruence qui contient ces égalités.

Structure d’equity graph (e-graph)

Ingrédients :

• Forêt de termes (rafinement, DAG de termes)
• Rafinement : partage, on représente dans la structure chaque terme une unique fois
• Union Find
• Invariant de congruence : fusionner les classes de l’UF selon l’axiome de congruence

Algorithmique des E Graphes

Un e-graphe affiche l’interface suivante :

• add qui prend en entrée un terme t.

  • Si t est déjà présent dans Rep(G), on renvoie la e-classe le représentant.
  • Sinon, on ajoute t à Rep(G) dans une nouvelle e-classe qui ne contient que lui.

  Algo :

  ADD(Terme h(t1,...tk)) :
    pour i allant de 1 à k :
        ci = ADD(ti)
    si N contient l'Enode h(c1,...ck) :
        renvoie la classe correspondante
    sinon :
        ajoute h(c1, ..., ck) à N
        ajoute une nouvelle Eclasse c à C
        ajoute (c, h(c1,...,ck)) à E
        renvoie c

• merge prend en entrée deux eclasses c_1 et c_2, et les fusionne. Algo :

  MERGE(Eclass c1, Eclass c2) :
    si c1 = c2:
        return # RAF
    Pour chaque Enode n in c2 :
        remplacer (c2, n) par (c1, n) dans E
    Pour chaque parent p = h(..., c2) :
        remplacer (p, c2) par (p, c1) dans E
    Pour chaque parent p de c1 :
        Pour chaque autre parent p' de c1 :
            Si p et p' ont le même symbole et ont les mêmes arcs sortants (dans le même ordre) :
                c = classe de p
                c' = classe de p'
                supprimer p' de l'Egraph
                MERGE(c,c')

• On a alors une procédure de décision QFEUF :

  DECIDE_QFEUF(Monome m) :
    créer un Egraph vide G
    pour chaque égalité t = u dans m :
        c1 = ADD(t)
        c2 = ADD(u)
        MERGE(c1,c2)
    pour chaque inégalité t != u dans m :
        c1 = ADD(t)
        c2 = ADD(u)
        si c1 = c2 : renvoyer UNSAT
    renvoyer SAT

  Cette procédure est correcte et complète.

Séance 6 : Instanciation des quantificateurs

Idée : On essaie de se ramener à des formules sans quantificateurs ?

Dans certaines théorie, il existe une procédure pour transformer toute formule \Phi en une formule \tilde{\Phi} équisatisfiable. Ces procédures n’existe pas dans le cas général, et sont souvent couteuses en calculs.

Cependant, pour montrer qu’une formule quantifiée est UNSAT, on peut juste exiber un contre exemple. Autrement trouver une instatiation des variables quantifiées qui la transforme en formule non quantifiée UNSAT, ce qui est calculable. On va donc essayer, dans la suite, de trouver une “bonne” instantiation.

On commence par se placer dans un cas d’étude restreint :

On considère les formules de la forme Q \land U où Q est une conjonction de formules avec quantificateurs et U est une CNF à formules sans quantificateurs.

On le fait sans perte de généralité.

Mise en forme des formules quantifiées

Dans Q on élimine les implications et on pousse les négations aux feuilles.

Gestion des \exists

Pour toute sous formule existencielle \exists x, \Phi(x) dans Q, on skolémise : On introduit un nouveau symbole e_x dans le langage et on remplace \exists x, \Phi(x) par \Phi(e_x).

/!\ : \forall x, \exists y, P(x,y) devient : \forall x, P(x, f_y(x))

Cela nous donne une formule équisatisfiable (cf cours de logique du premier ordre).

Gestion des \forall

Mise sous forme PCNF (Prenex CNF).
- On renomme les variables liées au \forall pour que chaque \forall ait sa variable unique.
- On fait remonter les \forall à la racine de la formule. - On obtient ainsi une formule équisatisfiable \forall x, y, z, ..., \Phi(x,y,z,...). On met \Phi en forme CNF.

Résultat

On se ramène à une formule Q \land U où U est une CNF sans quantificateurs (appelée faits de base) et Q est une conjonction de formules PCNF (on pourrait juste avoir une PCNF, mais pas très utile) appelée les universelles.

On va donc devoir utiliser un moteur d’instantiation pour tenter d’instancier les variables quantifiées universellements, pour la satisfiabilité :

Défi : Comment trouver les instanciations pertinentes ?

• Idée naïve : Essayer tout les termes de U.

• Instantiation par déclencheur (trigger) : Pour toute universelles, \forall x, ..., z, \Phi(x, ..., z) de Q. On sélectionne un déclencheur p(x, ..., z)

  • p(x, ..., z) est un terme qui apparait dans \Phi.
  • Toutes les variables x, ..., z apparaissent au moins une fois dans p.

  Fonctionnement : Si on observe dans U une instantiation p(t_x, ..., t_z) du déclencheur p, alors on ajoute \Phi(t_x, ..., t_z) aux faits de base.

  Exp :

  • \forall x,y, f(x,y) = f(y,x), on peut utiliser le déclencheur f(x, y)
  • \forall x,y, car(cons(x,y) = x, il y a plusieurs déclencheurs possibles : par exemple, cons(x,y), ou car(cons(x,y)). Ici, le premier permet de conclure, pas le deuxième.

  RQ (choix du déclencheur) :

  • Importance de la parsimonie : si un déclencheur p admet un déclencheur p' comme sous terme, p est plus restrictif et permettra moins souvent de conclure que p'.
  • Importance des performances : Si un déclencheur se déclenche trop, il va fortement dégrader les performances du solveur.
  • Certaines universelles nécessitent plus qu’un déclencheur :
    \forall x,y,z, g(x,y) = h(y,z) n’a pas de déclencheur unique, mais on peut déclencher l’instantiation sur un terme g(x,y) et un terme f(y,z)
  • Notre approche est incomplète (on n’arrive pas à prouver UNSAT sur certaines formules insatisfiables) et parfois ne termine pas :
    sur \forall x, f(f(x)) = x avec f(x) comme déclencheur, l’instantiation de cette universelle crée une nouvelle instance pour son déclencheur. C’est la boucle de déclenchement. On essaie de les éviter autant que possible.

E-matching

Le procédé de matching : recherche dans U des instanciations pour nos déclencheur.

En pratique, on stocke U dans un e-graph (car les théorie sont souvent dotées de la congruence).

Les e-graph proposent alors une opération nommée e-matching, adaptée à la recherche d’instanciations de déclencheurs.

Notations :

• Free(p) : ensemble des variables du déclencheur p.
• Étant donné un e-graph ((N,C),E), l’ensemble des substitutions est l’ensemble des fonctions Free(p) \rightarrow C

Procédé d’e-matching :

• Entrée : un déclencheur p.
• Sortie : l’ensemble des occurences de p dans l’e-graph.

Séance 7 : Théorie de l’arithmétique linéaire (Simplexe)

Ici, on va s’intéresser à des formules particulières :

On cherche à résoudre le problème suivant :

T_{LRA} := \{F | F_{SAT}\}

Ce problème est polynomial par programmation linéaire, d’après Dantzig (1947).

Problème en forme normale

On peut toujours représenter une instance de T_{LRA} par M = (A,B,N,(e_i), (u_i)) avec :

• A = (a_{i,j}) \in \mathbb{Q}^{mn}
• B est l’ensemble des variables \{x_i\}, de cardinal n (appelé variables de base)
• N est l’ensemble des variables \{x_j\}, disjoint de B, de cardinal m (variables hors base)
• (e_i) sont les m+n bornes inf \in \mathbb{Q} \cup \{-\infty\}
• (u_i) sont les m+n bornes sup \in \mathbb{Q} \cup \{+\infty\}

telle que :

F \in T_{LRA} équivalent à l’existence d’ube solution pour le problème S_M suivant :

• x_i = \sum_{x_j \in \mathbb{N}} a_{i,j} x_j, \forall x_i \in B
• \forall x_i \in B, \forall x_j \in N, e_i \leq x_i \leq u_i \land ej \leq x_j \leq u_j

Algorithme itératif

Invariants :

• (I_1) : \forall x_i \in B, \beta(x_i) = \sum_{x_j \in N} a_{i,j} \beta (x_j)
• (I_2) : \forall x_j \in N, e_j \leq \beta(x_j) \leq u_j
• (I_3) : F est SAT ssi S_M \neq \emptyset

On prend l’algorithme suivant :

L’état initial est \beta(_) = 0.

Tant que exists x_i in B, tq beta(x_i) < e_i ou beta(x_i) > u_i :
    SI on détecte S_M = vide : Renvoie UNSAT
    SINON : choisir x_j in N tel que :
        (M', beta') = PIVOT(M, beta, x_i, x_j)
        M', beta' satisfait (I_1) et (I_2) et S_M = vide <=> S_m' = vide

Démo :

• I_1 est vrai car 0 = \sum ... \times 0
• I_2 est vrai car N = \{\text{les variables initiales : non contraintes}\}
• I_3 est vrai par correction de mise en forme normale

Exemple :

N = \{x, y\}, B = \{s_1, s_2, s_3\}, \beta = 0

1er test de boucle :

\rightarrow \beta ne satisfait pas 2 \leq \beta(s_1). On veut “augmenter” \beta(s_1) jusqu’à 2, et on va permuter s_1 et x dans B et N.

Pivot de Gauss :

On exprime x en fonction de s_1 :

• x = s_1 - y
• s_2 = 2 (s_1 - y) - y = 2 s1 - 3 y
• s_3 = -(s_1 - y) + 2 y = y - s_1
• \beta'(y) = \beta(y) = 0
• \beta'(x) = 3
• \beta'(s_2) = 2 \beta'(s_1) + 3 \beta'(y) = 2 \times 2 - 3 \times 0 = 4
• \beta'(s_3) = - \beta'(s_1) + 3 \beta'(y) = -2 + 3 \times 0 = -2

(M, \beta) \leftarrow (M', \beta').

2e test de boucle :

\rightarrow il faut augmenter \beta(s_3) : -2 \rightarrow^{+3} 1

En augmentant \beta(y) de 1 :

Pivot de Gauss :

s_3 \leftrightarrow y

• y = \frac{1}{3} s_1 + \frac{1}{3} s_3
• x = s_1 - (\frac{1}{3} s_1 + \frac{1}{3} s_3) = \frac{2}{3} s_1 - \frac{1}{3} s_3
• s_2 = 2 s_1 - 3 y = s_1 - s_3

Alors :

• \beta'(s_3) = 1 (+3)
• \beta'(y) = 1 (+1)
• \beta'(x) = \frac{2}{3} 2 - \frac{1}{3} 1 = 1
• \beta'(s_2) = 2 - 1 = 1

Donc B = \{x, s_2, y\}, N = \{s_1, s_3\}

3e test de boucle :

FIN : F est SAT pour x = 1, y = 1

Séance 8 : Combinaison de théorie Nelson-Oppen

Motivation

Considérons F = (A_1 := f(f(x) - f(y))) \neq f(z) \land x < z \land y + z \leq x \land 0 \leq z

On se situe dans la théorie des fonctions non interprétées, donc pas LRA, et pas EUF car il n’y pas que des inégalités.

La méthode de Nelson Oppen permet alors de créer une théorie que l’on peut utiliser pour résoudre ce problème, en en réutilisant (et plus précisément en en combinant) des déjà connues. La théorie finale utilisée sera la théorie union.

/!\ : Limitation : Les théories considérées doivent être à signature disjointe.

Purification

Sépare F en sous formules pures.

Procédé :

La purification peut se faire de la manière suivante. Pour chaque sous terme de T_1 qui apparait dans un terme de T_2, on instancie une variable fraiche et une égalité.

Exemple sur le F de la motivation :

1. On introduit u pour f(x)
2. On introduit v pour f(y)
3. On introduit l’égalité u = f(x) \in EUF
4. On introduit l’égalité v = f(y) \in EUF
5. On introduit l’égalité w = u - v \in LRA
6. A_1 devient f(w) \neq f(z) \in EUF.

Le reste ne change pas, on obtient donc :

• F_1 = u = f(x) \land v = f(y) \land f(w) \neq f(z) \in EUF.
• F_2 = w = u - z \land x \leq y \land y + z \leq x \land 0 \leq z \in LRA

Algorithme

On peut alors créer un algorithme résolvant notre problème initial :

Nelson-Oppen(F):
    F1,F2 <- Purification(F)
    T1.assume(F1)
    T2.assume(F2)
    Tant que T1.sat() ou T2.sat() :
        Si il existe i,x,y tq Ti.propagate() equiv x=y:
            j <- 2 - i
            Tj.assume(x = y)
        Sinon renvoie SAT
    renvoie UNSAT

Exemple :

• Étape 0 : y + 0 \leq y + z \leq x \leq y donc x = y

• Étape 5 : u = v donc w = 0 et x = y donc z = 0. Donc x = z

  /!\ : On ne communique que des égalités entre variables, donc pas w = 0 par exemple !

Pour montrer la correction et la complètude de cet algorithme, on introduit la notion de convexité de théorie :

Exemples :

• EUF et LRA sont convexes.
• LIA (arithmétique linéaire sur \mathbb{Z}) n’est pas convexe.

Exemple de théorie non totalement infinie :

• T = \{\forall x, x = c\}
• \Sigma = \{c\}

Assertions de la logique de séparation

• Connecteurs logiques habituels (\lnot, \land, \lor, \implies, \exists, \forall)
• 2 nouveaux prédicats + 1 connecteur

Points-to

E,s \Downarrow l \in Loc F,s \Downarrow v \in Val

dom(h) = \right< l \left>, h(l) = v

Tas vide : emp

Conjonction séparante

Remarque : emp est neutre pour \ast.

On notera aussi : E \mapsto F_0, ..., F_n \equiv E \mapsto F_0 \ast E + 1 \mapsto F_1 \ast ... \ast E + n \mapsto F_n

Application aux listes chainées

MAIN WEBPAGE