diff --git a/ivette/src/frama-c/plugins/eva/api/general/index.ts b/ivette/src/frama-c/plugins/eva/api/general/index.ts
index 2e5a1eec5f83acdd15aae5b839502f64946bfe86..c37d5121b0b153e16622f7c4a2a01e83b54d3c20 100644
--- a/ivette/src/frama-c/plugins/eva/api/general/index.ts
+++ b/ivette/src/frama-c/plugins/eva/api/general/index.ts
@@ -113,6 +113,28 @@ const computationState_internal: State.Value<computationStateType> = {
 /** The current computation state of the analysis. */
 export const computationState: State.Value<computationStateType> = computationState_internal;
 
+const compute_internal: Server.ExecRequest<null,null> = {
+  kind: Server.RqKind.EXEC,
+  name: 'plugins.eva.general.compute',
+  input: Json.jNull,
+  output: Json.jNull,
+  fallback: null,
+  signals: [],
+};
+/** run eva analysis */
+export const compute: Server.ExecRequest<null,null>= compute_internal;
+
+const abort_internal: Server.GetRequest<null,null> = {
+  kind: Server.RqKind.GET,
+  name: 'plugins.eva.general.abort',
+  input: Json.jNull,
+  output: Json.jNull,
+  fallback: null,
+  signals: [],
+};
+/** abort eva analysis */
+export const abort: Server.GetRequest<null,null>= abort_internal;
+
 /** Callee function and caller stmt */
 export type CallSite = { call: decl, stmt: marker };
 
diff --git a/src/plugins/eva/api/general_requests.ml b/src/plugins/eva/api/general_requests.ml
index ec649515e95eabd457e0263c5db12ce4f0abc597..c5cba410e23c386073a573169696b59005e06b61 100644
--- a/src/plugins/eva/api/general_requests.ml
+++ b/src/plugins/eva/api/general_requests.ml
@@ -55,6 +55,22 @@ let computation_signal =
     ~output:(module ComputationState)
     (module Self.ComputationState)
 
+let () = Request.register ~package
+    ~kind:`EXEC
+    ~name:"compute"
+    ~descr:(Markdown.plain "run eva analysis")
+    ~input:(module Data.Junit)
+    ~output:(module Data.Junit)
+    Analysis.compute
+
+let () = Request.register ~package
+    ~kind:`GET (* able to interrupt the EXEC compute request *)
+    ~name:"abort"
+    ~descr:(Markdown.plain "abort eva analysis")
+    ~input:(module Data.Junit)
+    ~output:(module Data.Junit)
+    Analysis.abort
+
 (* ----- Callers & Callees -------------------------------------------------- *)
 
 module CallSite =
diff --git a/src/plugins/eva/engine/analysis.ml b/src/plugins/eva/engine/analysis.ml
index 35c262f48a1521c73ef8a8ea43de22c78aa67c84..c3b9861d3fd1c0dc50cc68dd5f1fef6872cc18dc 100644
--- a/src/plugins/eva/engine/analysis.ml
+++ b/src/plugins/eva/engine/analysis.ml
@@ -217,7 +217,10 @@ let force_compute () =
   (* The new analyzer can be accesed through hooks *)
   Self.ComputationState.set Computing;
   let module Analyzer = (val snd !ref_analyzer) in
-  Analyzer.compute_from_entry_point ~lib_entry kf
+  try Analyzer.compute_from_entry_point ~lib_entry kf
+  with Self.Abort ->
+    Self.(ComputationState.set Aborted);
+    Self.error "The analysis has been aborted: results are incomplete."
 
 let compute () =
   (* Nothing to recompute when Eva has already been computed. This boolean
@@ -233,3 +236,7 @@ let () = Parameters.ForceValues.set_output_dependencies [Self.state]
 
 let main () = if Parameters.ForceValues.get () then compute ()
 let () = Boot.Main.extend main
+
+let abort () =
+  if Self.ComputationState.get () = Computing
+  then Iterator.signal_abort ~kill:false
diff --git a/src/plugins/eva/engine/analysis.mli b/src/plugins/eva/engine/analysis.mli
index 736b503e7facf164c0684625919b4af39878cf5c..436a53aa7c6bfe741bae59843edd0a913002cce6 100644
--- a/src/plugins/eva/engine/analysis.mli
+++ b/src/plugins/eva/engine/analysis.mli
@@ -77,6 +77,10 @@ val register_hook: ((module S) -> unit) -> unit
 val force_compute : unit -> unit
 (** Perform a full analysis, starting from the [main] function. *)
 
+val abort : unit -> unit
+(** Cleanly abort the analysis at the next safe point: partial results will be
+    saved and Frama-C is not killed. *)
+
 [@@@ api_start]
 val compute : unit -> unit
 (** Computes the Eva analysis, if not already computed, using the entry point
diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml
index e853b106bab8ca3ae07819bcf83981026a8de1ad..a3bd81ebe62d3c50591a9acfb9368ae0cc733e7c 100644
--- a/src/plugins/eva/engine/compute_functions.ml
+++ b/src/plugins/eva/engine/compute_functions.ml
@@ -88,6 +88,7 @@ let generate_specs () =
   Parameters.UsePrototype.iter aux
 
 let pre_analysis () =
+  Iterator.signal_reset ();
   floats_ok ();
   options_ok ();
   plugins_ok ();
@@ -139,7 +140,7 @@ let register_signal_handler () =
   let warn () =
     Self.warning ~once:true "Stopping analysis at user request@."
   in
-  let stop _ = warn (); Iterator.signal_abort () in
+  let stop _ = warn (); Iterator.signal_abort ~kill:true in
   let interrupt _ = warn (); raise Sys.Break in
   let register_handler signal handler =
     match Sys.signal signal (Sys.Signal_handle handler) with
diff --git a/src/plugins/eva/engine/iterator.ml b/src/plugins/eva/engine/iterator.ml
index f4d84b5a63efd47c627c14758fb2effec2b1fce2..35f3fda11c223b760e6e8a9d24412ccbe2938594 100644
--- a/src/plugins/eva/engine/iterator.ml
+++ b/src/plugins/eva/engine/iterator.ml
@@ -26,14 +26,16 @@ open Eva_automata
 open Lattice_bounds
 open Bottom.Operators
 
-let check_signals, signal_abort =
-  let signal_emitted = ref false in
-  (fun () ->
-     if !signal_emitted then begin
-       signal_emitted := false;
-       raise Sys.Break
-     end),
-  (fun () -> signal_emitted := true)
+type signal = Abort | Kill
+
+let signal_emitted = ref None
+let signal_abort ~kill = signal_emitted := Some (if kill then Kill else Abort)
+let signal_reset () = signal_emitted := None
+
+let check_signals () =
+  Option.iter
+    (fun signal -> raise (if signal = Kill then Sys.Break else Self.Abort))
+    !signal_emitted
 
 let dkey = Self.dkey_iterator
 let stat_iterations = Statistics.register_statement_stat "iterations"
diff --git a/src/plugins/eva/engine/iterator.mli b/src/plugins/eva/engine/iterator.mli
index a1b632ba703a17e4c04c9052e6680d529e8e1c1a..b898e9e8663283ef824fb0599e9e93e2c0ee811a 100644
--- a/src/plugins/eva/engine/iterator.mli
+++ b/src/plugins/eva/engine/iterator.mli
@@ -22,8 +22,11 @@
 
 open Cil_types
 
-(** Mark the analysis as aborted. It will be stopped at the next safe point *)
-val signal_abort: unit -> unit
+(** Mark the analysis as aborted: it will be stopped at the next safe point. *)
+val signal_abort: kill:bool -> unit
+
+(** Reset the signal sent by [signal_abort], if any. *)
+val signal_reset: unit -> unit
 
 (** Provided [stmt] is an 'if' construct, [fst (condition_truth_value stmt)]
     (resp. snd) is true if and only if the condition of the 'if' has been
diff --git a/src/plugins/eva/self.ml b/src/plugins/eva/self.ml
index d2e1e284de6f5f393a52c919d1d676c6505ccf50..590a2a4da92a50c211b21900b97a11579ea6568c 100644
--- a/src/plugins/eva/self.ml
+++ b/src/plugins/eva/self.ml
@@ -67,6 +67,8 @@ struct
   include (State_builder.Ref (Datatype') (Prototype))
 end
 
+exception Abort
+
 let is_computed () =
   match ComputationState.get () with
   | Computed | Aborted -> true
diff --git a/src/plugins/eva/self.mli b/src/plugins/eva/self.mli
index ab724f59bbc5455c7754f76d9a694b2ec39e4304..4872dcfaa89771be3000d36644addbf7b5a76f93 100644
--- a/src/plugins/eva/self.mli
+++ b/src/plugins/eva/self.mli
@@ -35,6 +35,9 @@ type computation_state = NotComputed | Computing | Computed | Aborted
     [force_compute] and states updates. *)
 module ComputationState : State_builder.Ref with type data = computation_state
 
+(** Exception used to cleanly abort the analysis (without killing Frama-C). *)
+exception Abort
+
 (** Debug categories responsible for printing initial and final states of Value.
     Enabled by default, but can be disabled via the command-line:
     -value-msg-key="-initial_state,-final_state" *)
diff --git a/src/plugins/eva/utils/eva_utils.ml b/src/plugins/eva/utils/eva_utils.ml
index ad3e6bec741090f1008cdba2e354223c45ab380a..f8da531466ce7d087c4a37df41e232e67fa5fdb2 100644
--- a/src/plugins/eva/utils/eva_utils.ml
+++ b/src/plugins/eva/utils/eva_utils.ml
@@ -138,8 +138,9 @@ let protect f ~cleanup =
   with
   | Log.AbortError _ | Log.AbortFatal _ | Log.FeatureRequest _
   | Sys.Break as e when catch () ->
-    cleanup ();
-    raise e
+    cleanup (); raise e
+  | Self.Abort as e ->
+    cleanup (); raise e
 
 let register_new_var v typ =
   if Cil.isFunctionType typ then