diff --git a/src/plugins/e-acsl/doc/memory_model/article.pdf b/src/plugins/e-acsl/doc/memory_model/article.pdf
index 720206c4d5bcd748d1d07a4975dd6fe038e610aa..b00f251e110513423e61ce008e590bc54554c3cb 100644
Binary files a/src/plugins/e-acsl/doc/memory_model/article.pdf and b/src/plugins/e-acsl/doc/memory_model/article.pdf differ
diff --git a/src/plugins/e-acsl/doc/memory_model/article.tex b/src/plugins/e-acsl/doc/memory_model/article.tex
index 67e401ee44a175dce1001d58e02a2a231a87f5f4..3f635e815f5272557119563820bab297dd26db0e 100644
--- a/src/plugins/e-acsl/doc/memory_model/article.tex
+++ b/src/plugins/e-acsl/doc/memory_model/article.tex
@@ -692,18 +692,14 @@ $ptr$ are initialized, 0 otherwise.
\begin{tabular}{|c|c|c|c|c|c|c|}
\hline
& alarms & time & test cases & mutants & mutants killed \\
- %\hline
- %$p_1$ & 5 & 22s & 27 & 2 & 2 \\ % sorted
- %\hline
- %$p_2$ & 19 & 34s & 31 & 6 & 6 \\ % f
\hline
$fibonacci$ & 31 & 54s & 38 & 20 & 20 \\
\hline
- $Bsearch$ & 25 & 65s & 20 & 43 & 43 \\
+ $Bsearch$ & 28 & 63s & 20 & 41 & 41 \\
\hline
- $Bsort$ & 32 & 200s & 153 & 50 & 50 \\
+ $Bsort$ & 37 & 273s & 153 & 45 & 47 \\
\hline
- $Merge$ & 52 & 106s & 19 & 63 & 63 \\
+ $Merge$ & 55 & 100s & 19 & 58 & 58 \\
\hline
$BubbleSort$ & 31 & 963s & 873 & 44 & 44 \\
\hline
diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/Bsearch/bsearch.c b/src/plugins/e-acsl/doc/memory_model/experiments/Bsearch/bsearch.c
new file mode 100644
index 0000000000000000000000000000000000000000..12938539bbf92154edb6eed3ca4d068fc46b66b5
--- /dev/null
+++ b/src/plugins/e-acsl/doc/memory_model/experiments/Bsearch/bsearch.c
@@ -0,0 +1,65 @@
+/* run.config
+ COMMENT: BsearchPrecond
+ OPT: -pc -pc-trace -pc-tests -kernel-debug 0 -verbose 0 -pc-deter -pc-trace-preconds -pc-trace-simpred -pc-trace-result -main Bsearch
+*/
+/* Binary search of a given element in a given ordered array
+ returning 1 if the element is present and 0 if not.
+ This example is like Bsearch
+ but gives an example of
+ a precondition coded in C */
+
+/*@ ensures (\exists int i; 0 <= i < 10 && A[i] == elem) <==> \result;
+ @*/
+int Bsearch( int A[10], int elem)
+{
+ int low, high, mid, found ;
+
+ low = 0 ;
+ high = 9 ;
+ found = 0 ;
+ while( ( high > low ) )
+ {
+ //@ assert high > low;
+ mid = (low + high) / 2 ;
+ //@ assert mid == (low+high) / 2;
+ if( elem == A[mid] ) {
+ //@ assert elem == A[mid];
+ found = 1;
+ //@ assert found == 1;
+ }
+ if( elem > A[mid] ) {
+ //@ assert elem > A[mid];
+ low = mid + 1 ;
+ //@ assert low == mid + 1;
+ }
+ else {
+ //@ assert elem <= A[mid];
+ high = mid - 1;
+ //@ assert high == mid - 1;
+ }
+ }
+ //@ assert high <= low;
+ mid = (low + high) / 2 ;
+ //@ assert mid == (low+high) / 2;
+
+ if( ( found != 1) && ( elem == A[mid]) ) {
+ //@ assert found != 1 && elem == A[mid];
+ found = 1;
+ //@ assert found == 1;
+ }
+
+ return found ;
+}
+
+/* C precondition of function Bsearch
+ This must have the name of the tested function suffixed with _precond
+ and have the same number of arguments with the same types.
+ It must return 1 if the parameter values satisfy the precondition and 0 if not */
+int Bsearch_precond( int A[10], int elem) {
+ int i;
+ for (i = 0; i < 9; i++){
+ if (A[i]>A[i+1])
+ return 0 ; /* not ordered by increasing value */
+ }
+ return 1;
+}
diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/Bsearch/test_parameters_Bsearch.pl b/src/plugins/e-acsl/doc/memory_model/experiments/Bsearch/test_parameters_Bsearch.pl
new file mode 100644
index 0000000000000000000000000000000000000000..a06b2298d3a8a919db611057f2fb6a01f883417a
--- /dev/null
+++ b/src/plugins/e-acsl/doc/memory_model/experiments/Bsearch/test_parameters_Bsearch.pl
@@ -0,0 +1,29 @@
+:- module(test_parameters).
+
+:- import create_input_val/3 from substitution.
+
+:- export dom/4.
+:- export create_input_vals/2.
+:- export unquantif_preconds/2.
+:- export quantif_preconds/2.
+:- export strategy/2.
+:- export precondition_of/2.
+
+dom('Bsearch',cont('A',_),[],int([0..100])).
+dom('pathcrawler__Bsearch_precond',A,B,C):-
+ dom('Bsearch',A,B,C).
+
+create_input_vals('Bsearch',Ins):-
+ create_input_val('elem',int([0..100]),Ins),
+ create_input_val(dim('A'),int([10]),Ins),
+ true.
+create_input_vals('Bsearch',Ins):-
+ create_input_vals('pathcrawler__Bsearch_precond',Ins).
+
+unquantif_preconds('Bsearch',[]).
+quantif_preconds('Bsearch',[]).
+
+strategy('Bsearch',[]).
+strategy('pathcrawler__Bsearch_precond',[]).
+
+precondition_of('Bsearch','pathcrawler__Bsearch_precond').
diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/Bsort/bsort.c b/src/plugins/e-acsl/doc/memory_model/experiments/Bsort/bsort.c
new file mode 100644
index 0000000000000000000000000000000000000000..007fede5caf07e1e225e19bd6a6f63967eb8cc27
--- /dev/null
+++ b/src/plugins/e-acsl/doc/memory_model/experiments/Bsort/bsort.c
@@ -0,0 +1,50 @@
+/* run.config
+ COMMENT: Bsort
+ OPT: -pc -pc-trace -pc-tests -kernel-debug 0 -verbose 0 -pc-deter -pc-trace-preconds -pc-trace-simpred -pc-trace-result -main bsort
+*/
+/* Bubble sort of a given array 'table' of a given length 'l' in descending order. This example is interesting because of its
+ - variable dimension input array
+ - loop with a variable number of iterations,
+ which is limited by limiting the array dimension
+ - oracle which does not sort but checks the result is ordered */
+
+/*@ ensures \forall int k; 0 <= k < l-1 ==> table[k] >= table[k+1];
+ @*/
+void bsort (int * table, int l)
+{
+ int i, temp, nb;
+ char fini;
+ fini = 0;
+ nb = 0;
+ //@ assert l >= 0;
+ //@ assert fini == 0;
+ //@ assert nb == 0;
+ while ( !fini && (nb < l-1)){
+ //@ assert fini == 0;
+ //@ assert nb < l-1;
+ fini = 1;
+ //@ assert fini == 1;
+ for (i=0 ; i<l-1 ; ) {
+ //@ assert 0 <= i < l-1;
+ if (table[i] < table[i+1]){
+ //@ assert table[i] < table[i+1];
+ fini = 0;
+ //@ assert fini == 0;
+ temp = table[i];
+ //@ assert temp == table[i];
+ table[i] = table[i + 1];
+ //@ assert table[i] == table[i+1];
+ table[i + 1] = temp;
+ //@ assert table[i+1] == temp;
+ }
+ //@ ghost int old_i = i;
+ i++;
+ //@ assert old_i + 1 == i;
+ }
+ //@ assert i >= l-1;
+ //@ ghost int old_nb = nb;
+ nb++;
+ //@ assert old_nb + 1 == nb;
+ }
+ //@ assert fini == 1 || nb >= l-1;
+}
diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/Bsort/test_parameters_bsort.pl b/src/plugins/e-acsl/doc/memory_model/experiments/Bsort/test_parameters_bsort.pl
new file mode 100644
index 0000000000000000000000000000000000000000..ad41d5bb9f4b647beee36eb30390da452acad731
--- /dev/null
+++ b/src/plugins/e-acsl/doc/memory_model/experiments/Bsort/test_parameters_bsort.pl
@@ -0,0 +1,24 @@
+:- module(test_parameters).
+
+:- import create_input_val/3 from substitution.
+
+:- export dom/4.
+:- export create_input_vals/2.
+:- export unquantif_preconds/2.
+:- export quantif_preconds/2.
+:- export strategy/2.
+:- export precondition_of/2.
+
+dom('bsort',cont('table',_),[],int([-100..100])).
+
+create_input_vals('bsort',Ins):-
+ create_input_val(dim('table'),int([0..5]),Ins),
+ create_input_val('l',int([0..5]),Ins),
+ true.
+
+unquantif_preconds('bsort',[cond(egal,dim('table'),'l',pre)]).
+quantif_preconds('bsort',[]).
+
+strategy('bsort',[]).
+
+precondition_of(0,0).
diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/BubbleSort/bubblesort.c b/src/plugins/e-acsl/doc/memory_model/experiments/BubbleSort/bubblesort.c
new file mode 100644
index 0000000000000000000000000000000000000000..415b567a1d426a3b55603c159c464ccb80d7e450
--- /dev/null
+++ b/src/plugins/e-acsl/doc/memory_model/experiments/BubbleSort/bubblesort.c
@@ -0,0 +1,44 @@
+
+/*@ ensures \forall int i; 0 <= i < length-1 ==> a[i] <= a[i+1];
+ @*/
+void bubble_sort(int* a, int length)
+{
+ int auf = 1;
+ int ab;
+ int fixed_auf = 1;
+
+
+ for (; auf < length; )
+ {
+ //@ assert auf < length;
+ fixed_auf = auf;
+ ab=auf;
+
+ while (0 < ab && a[ab] < a[ab-1])
+ {
+ //@ assert 0 < ab;
+ //@ assert a[ab] < a[ab-1];
+ //@ ghost int old_1 = a[ab];
+ //@ ghost int old_2 = a[ab-1];
+ int temp = a[ab];
+ a[ab] = a[ab-1];
+ a[ab-1] = temp;
+
+ //@ assert old_1 == a[ab-1];
+ //@ assert old_2 == a[ab];
+
+ //@ ghost int old_ab = ab;
+ ab = ab-1;
+ //@ assert old_ab - 1 == ab;
+ }
+ //@ assert 0 >= ab || a[ab] >= a[ab-1];
+
+ //@ ghost int old_auf = auf;
+ auf++;
+ //@ assert old_auf + 1 == auf;
+
+ fixed_auf = auf;
+ }
+ //@ assert auf >= length;
+}
+
diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/BubbleSort/test_parameters.pl b/src/plugins/e-acsl/doc/memory_model/experiments/BubbleSort/test_parameters.pl
new file mode 100644
index 0000000000000000000000000000000000000000..0ae92b1c264ca21bff1df37a9c291fdca40e8dff
--- /dev/null
+++ b/src/plugins/e-acsl/doc/memory_model/experiments/BubbleSort/test_parameters.pl
@@ -0,0 +1,21 @@
+:- module(test_parameters).
+:- import create_input_val/3 from substitution.
+:- export dom/4.
+:- export create_input_vals/2.
+:- export unquantif_preconds/2.
+:- export quantif_preconds/2.
+:- export strategy/2.
+:- export precondition_of/2.
+
+dom('bubble_sort',cont('a',_),[],int([-20..20])).
+
+create_input_vals('bubble_sort',Ins):-
+ create_input_val(dim('a'),int([0..6]),Ins),
+ create_input_val('length',int([0..6]),Ins),
+ true.
+
+unquantif_preconds('bubble_sort',[cond(egal,dim('a'),'length',pre)]).
+
+quantif_preconds('bubble_sort',[]).
+strategy('bubble_sort',[]).
+precondition_of(0,0).
diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/Merge/merge.c b/src/plugins/e-acsl/doc/memory_model/experiments/Merge/merge.c
new file mode 100644
index 0000000000000000000000000000000000000000..2787cc569d130ad591e4eb666ed68c4101f307c2
--- /dev/null
+++ b/src/plugins/e-acsl/doc/memory_model/experiments/Merge/merge.c
@@ -0,0 +1,63 @@
+/* run.config
+ OPT: -pc -pc-trace -pc-tests -kernel-debug 0 -verbose 0 -pc-deter -pc-trace-preconds -pc-trace-simpred -pc-trace-result -pc-k-path 2 -main Merge
+*/
+
+
+
+
+/*@ ensures \forall int i; 0 <= i < (l1+l2-1) ==> t3[i] <= t3[i+1];
+ @*/
+void Merge (int t1[], int t2[], int t3[], int l1, int l2) {
+ int i = 0;
+ int j = 0;
+ int k = 0;
+
+ while (i < l1 && j < l2) {
+ //@ assert i < l1;
+ //@ assert j < l2;
+ if (t1[i] < t2[j]) {
+ //@ assert t1[i] < t2[j];
+ t3[k] = t1[i];
+ //@ assert t3[k] == t1[i];
+ //@ ghost int tmp = i;
+ i++;
+ //@ assert tmp + 1 == i;
+ }
+ else {
+ //@ assert t1[i] >= t2[j];
+ t3[k] = t2[j];
+ //@ assert t3[k] == t2[j];
+ //@ ghost int tmp = j;
+ j++;
+ //@ assert tmp + 1 == j;
+ }
+ //@ ghost int tmp = k;
+ k++;
+ //@ assert tmp + 1 == k;
+ }
+ //@ assert i >= l1 || j >= l2;
+ while (i < l1) {
+ //@ assert i < l1;
+ t3[k] = t1[i];
+ //@ assert t3[k] == t1[i];
+ //@ ghost int tmp1 = i;
+ //@ ghost int tmp2 = k;
+ i++;
+ //@ assert tmp1 + 1 == i;
+ k++;
+ //@ assert tmp2 + 1 == k;
+ }
+ //@ assert i >= l1;
+ while (j < l2) {
+ //@ assert j < l2;
+ t3[k] = t2[j];
+ //@ assert t3[k] == t2[j];
+ //@ ghost int tmp1 = j;
+ //@ ghost int tmp2 = k;
+ j++;
+ //@ assert tmp1 + 1 == j;
+ k++;
+ //@ assert tmp2 + 1 == k;
+ }
+ //@ assert j >= l2;
+}
diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/Merge/test_parameters_Merge.pl b/src/plugins/e-acsl/doc/memory_model/experiments/Merge/test_parameters_Merge.pl
new file mode 100644
index 0000000000000000000000000000000000000000..44c0551ba13f14061162865add7be382c3340a8e
--- /dev/null
+++ b/src/plugins/e-acsl/doc/memory_model/experiments/Merge/test_parameters_Merge.pl
@@ -0,0 +1,77 @@
+:- module(test_parameters).
+
+:- import create_input_val/3 from substitution.
+
+:- export dom/4.
+:- export create_input_vals/2.
+:- export unquantif_preconds/2.
+:- export quantif_preconds/2.
+:- export strategy/2.
+:- export precondition_of/2.
+
+dom('Merge',cont('t1',_),[],int([-10..10])).
+dom('Merge',cont('t2',_),[],int([-10..10])).
+
+create_input_vals('Merge',Ins):-
+ create_input_val(dim('t1'),int([0..10]),Ins),
+ create_input_val(dim('t2'),int([0..10]),Ins),
+ create_input_val(dim('t3'),int([0..20]),Ins),
+ create_input_val('l1',int([0..10]),Ins),
+ create_input_val('l2',int([0..10]),Ins),
+ true.
+
+unquantif_preconds('Merge',
+ [cond(supegal,dim('t1'),'l1',pre),
+ cond(supegal,dim('t2'),'l2',pre),
+ cond(supegal,dim('t3'),+(int(math),'l1','l2'),pre)]).
+quantif_preconds('Merge',[uq_cond([UQV3],
+ [cond(supegal,UQV3,1,pre)],
+ supegal,
+ cont('t1',UQV3),
+ cont('t1',-(int(math),UQV3,1))),
+ uq_cond([UQV4],
+ [cond(supegal,UQV4,1,pre)],
+ supegal,
+ cont('t2',UQV4),
+ cont('t2',-(int(math),UQV4,1)))]).
+
+strategy('Merge',[kpath(2)]).
+
+precondition_of(0,0).
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/fibonacci/fibo.c b/src/plugins/e-acsl/doc/memory_model/experiments/fibonacci/fibo.c
new file mode 100644
index 0000000000000000000000000000000000000000..7d841734de9784350b3e34920bf69b87a2c0e06b
--- /dev/null
+++ b/src/plugins/e-acsl/doc/memory_model/experiments/fibonacci/fibo.c
@@ -0,0 +1,23 @@
+
+/*@ requires n >= 3;
+ @ ensures t[0] == 1;
+ @ ensures t[1] == 1;
+ @ ensures \forall int i; 2 <= i < n ==> t[i-2] + t[i-1] == t[i];
+ @*/
+void fibo(int *t, int n) {
+ int i;
+ t[0] = t[1] = 1;
+ //@ assert t[0] == 1;
+ //@ assert t[1] == 1;
+
+ //@ assert n >= 3;
+ for(i = 2; i < n; ) {
+ //@ assert 2 <= i < n;
+ t[i] = t[i-1] + t[i-2];
+ //@ assert t[i] == t[i-1] + t[i-2];
+ //@ ghost int old_i = i;
+ i++;
+ //@ assert old_i + 1 == i;
+ }
+ //@ assert i >= n;
+}
diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/fibonacci/test_parameters_fibo.pl b/src/plugins/e-acsl/doc/memory_model/experiments/fibonacci/test_parameters_fibo.pl
new file mode 100644
index 0000000000000000000000000000000000000000..04fefca54bd2d9315f7ddef244f53d76ca8ebfb2
--- /dev/null
+++ b/src/plugins/e-acsl/doc/memory_model/experiments/fibonacci/test_parameters_fibo.pl
@@ -0,0 +1,19 @@
+:- module(test_parameters).
+:- import create_input_val/3 from substitution.
+:- export dom/4.
+:- export create_input_vals/2.
+:- export unquantif_preconds/2.
+:- export quantif_preconds/2.
+:- export strategy/2.
+:- export precondition_of/2.
+
+dom('fibo', cont('t',_), [], int([-10..10])).
+create_input_vals('fibo', Ins):-
+ create_input_val('n', int([3..40]),Ins),
+ create_input_val(dim('t'), int([3..40]),Ins),
+ true.
+
+quantif_preconds('fibo',[]).
+unquantif_preconds('fibo',[cond(egal,dim('t'),'n',pre)]).
+strategy('fibo',[]).
+precondition_of(0,0).