diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml
index cfb195799f725002717bd4354080abf90cfa08fd..1e79de5680ef53ea6fea9c70bd325b74bc0a5cee 100644
--- a/src/plugins/eva/engine/compute_functions.ml
+++ b/src/plugins/eva/engine/compute_functions.ml
@@ -363,6 +363,7 @@ module Make (Abstract: Abstractions.Eva) = struct
       post_analysis ();
       Abstract.Dom.post_analysis final_state;
       Summary.print_summary ();
+      Statistics.export_as_csv ();
       restore_signals ()
     in
     let cleanup () =
diff --git a/src/plugins/eva/engine/iterator.ml b/src/plugins/eva/engine/iterator.ml
index c05c4a2f10b16094f37ca59e57c63161cf4f5389..2ccf27969ed46fad6a08704b096a9ecf824fc026 100644
--- a/src/plugins/eva/engine/iterator.ml
+++ b/src/plugins/eva/engine/iterator.ml
@@ -36,6 +36,7 @@ let check_signals, signal_abort =
 
 let dkey = Self.dkey_iterator
 let dkey_callbacks = Self.dkey_callbacks
+let stat_iterations = Statistics.register_statement_stat "iterations"
 
 let blocks_share_locals b1 b2 =
   match b1.blocals, b2.blocals with
@@ -562,6 +563,7 @@ module Make_Dataflow
         not (process_vertex ~widening:true v) || !iteration_count = 0
       do
         Self.debug ~dkey "iteration %d" !iteration_count;
+        Option.iter (Statistics.incr stat_iterations) v.vertex_start_of;
         iterate_list w;
         incr iteration_count;
       done;
diff --git a/src/plugins/eva/engine/mem_exec.ml b/src/plugins/eva/engine/mem_exec.ml
index 71a68968d66278547885435ca8aae20ffc1e569b..a4a530a9741beeddfabb84ce64c3b793ee629878 100644
--- a/src/plugins/eva/engine/mem_exec.ml
+++ b/src/plugins/eva/engine/mem_exec.ml
@@ -20,6 +20,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+let stat_hits = Statistics.register_function_stat "memexec-hits"
+let stat_misses = Statistics.register_function_stat "memexec-misses"
 
 module SaveCounter =
   State_builder.SharedCounter(struct let name = "Mem_exec.save_counter" end)
@@ -263,10 +265,14 @@ module Make
       let args = List.map (function `Bottom -> None | `Value v -> Some v) args in
       let previous = ActualArgs.Map.find args previous_kf in
       find_match_in_previous kf previous state;
+      Statistics.incr stat_misses kf;
       None
     with
-    | Not_found -> None
+    | Not_found ->
+      Statistics.incr stat_misses kf;
+      None
     | Result_found (outputs, i) ->
+      Statistics.incr stat_hits kf;
       let call_result = outputs in
       Some (call_result, i)
 
diff --git a/src/plugins/eva/partitioning/partitioning_index.ml b/src/plugins/eva/partitioning/partitioning_index.ml
index 8379820d3bff92866607ee46d8f34b1065d6541d..422d29c424b36cfd050c73f464ae880d6c6cbf62 100644
--- a/src/plugins/eva/partitioning/partitioning_index.ml
+++ b/src/plugins/eva/partitioning/partitioning_index.ml
@@ -20,6 +20,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
+let stat_hits = Statistics.register_global_stat "partitioning-index-hits"
+let stat_misses = Statistics.register_global_stat "partitioning-index-misses"
+
+
 (** Partition of the abstract states, computed for each node by the
     dataflow analysis. *)
 module Make (Domain : Abstract.Domain.External)
@@ -86,6 +90,11 @@ module Make (Domain : Abstract.Domain.External)
         then false
         else (Index.add states prefix state; true)
 
+  let add state partition =
+    let r = add state partition in
+    Statistics.incr (if r then stat_misses else stat_hits) ();
+    r
+
   let iter f { states; others } =
     Index.iter (fun _k v -> f v) states;
     List.iter f others
diff --git a/src/plugins/eva/partitioning/trace_partitioning.ml b/src/plugins/eva/partitioning/trace_partitioning.ml
index ea47c4aa9a23114915f126f9062413b27b10fc41..6e0868ccf242c011ba4763e2f0a5649a59eaae2f 100644
--- a/src/plugins/eva/partitioning/trace_partitioning.ml
+++ b/src/plugins/eva/partitioning/trace_partitioning.ml
@@ -23,6 +23,8 @@
 open Cil_types
 open Partition
 
+let stat_max_widenings = Statistics.register_statement_stat "max-widenings"
+
 module Make
     (Abstract: Abstractions.Eva)
     (Kf : sig val kf: kernel_function end) =
@@ -59,6 +61,7 @@ struct
     mutable widened_state : state option;
     mutable previous_state : state;
     mutable widening_counter : int;
+    mutable widening_steps : int; (* count the number of successive widenings *)
   }
 
   type widening = {
@@ -336,6 +339,8 @@ struct
           w.previous_state <- next;
           w.widened_state <- Some next;
           w.widening_counter <- widening_period - 1;
+          w.widening_steps <- w.widening_steps + 1;
+          Statistics.grow stat_max_widenings stmt w.widening_steps;
           Some next
         end
       with Not_found ->
@@ -345,7 +350,9 @@ struct
           let ws =
             { widened_state = None;
               previous_state = curr;
-              widening_counter = widening_delay - 1; }
+              widening_counter = widening_delay - 1;
+              widening_steps = 0
+            }
           in
           w.widening_partition <- Partition.replace key ws w.widening_partition
         end;