diff --git a/src/analyses/tutorials/constants.ml b/src/analyses/tutorials/constants.ml
index cd40d6ffe5..058f2c32f0 100644
--- a/src/analyses/tutorials/constants.ml
+++ b/src/analyses/tutorials/constants.ml
@@ -2,13 +2,18 @@
 
 open GoblintCil
 open Analyses
+open SimplifiedAnalysis
 
 (** An analysis specification for didactic purposes.
  It only considers definite values of local variables.
  We do not pass information interprocedurally. *)
-module Spec : Analyses.MCPSpec =
+module Spec : SimplifiedSpec =
 struct
-  let name () = "constants"
+  include SimplifiedAnalysis.DefaultSpec
+
+  let name = "constants"
+  module V = Printable.Unit
+  module G = Lattice.Unit
 
   module I = IntDomain.Flattened
 
@@ -16,7 +21,7 @@ struct
   module D = MapDomain.MapBot (Basetype.Variables) (I)
 
   (* No contexts *)
-  include Analyses.IdentityUnitContextsSpec
+  module C = Printable.Unit
 
   let get_local = function
     | Var v, NoOffset when isIntegralType v.vtype && not (v.vglob || v.vaddrof) -> Some v (* local integer variable whose address is never taken *)
@@ -44,29 +49,29 @@ struct
     | _ -> I.top ()
 
   (* transfer functions *)
-  let assign man (lval:lval) (rval:exp) : D.t =
+
+  let assign man state (lval:lval) (rval:exp) : D.t =
     match get_local lval with
-    | Some loc -> D.add loc (eval man.local rval) man.local
-    | None -> man.local
+    | Some loc -> D.add loc (eval state rval) state
+    | None -> state
 
-  let branch man (exp:exp) (tv:bool) : D.t =
-    let v = eval man.local exp in
+  let branch man state (exp:exp) (tv:bool) : D.t =
+    let v = eval state exp in
     match I.to_bool v with
       | Some b when b <> tv -> raise Deadcode (* if the expression evaluates to not tv, the tv branch is not reachable *)
-      | _ -> man.local
+      | _ -> state
 
-  let body man (f:fundec) : D.t =
+  let body man state (f:fundec) : D.t =
     (* Initialize locals to top *)
-    List.fold_left (fun m l -> D.add l (I.top ()) m) man.local f.slocals
+    List.fold_left (fun m l -> D.add l (I.top ()) m) state f.slocals
 
-  let return man (exp:exp option) (f:fundec) : D.t =
+  let return man state (exp:exp option) (f:fundec) : D.t =
     (* Do nothing, as we are not interested in return values for now. *)
-    man.local
+    state
 
-  let enter man (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
+  let enter man caller_state (lval: lval option) (f:fundec) (args: exp list) : D.t =
     (* Set the formal int arguments to top *)
-    let callee_state = List.fold_left (fun m l -> D.add l (I.top ()) m) (D.bot ()) f.sformals in
-    [(man.local, callee_state)]
+    List.fold_left (fun m l -> D.add l (I.top ()) m) (D.bot ()) f.sformals
 
   let set_local_int_lval_top (state: D.t) (lval: lval option) =
     match lval with
@@ -77,22 +82,19 @@ struct
         )
       |_ -> state
 
-  let combine_env man lval fexp f args fc au f_ask =
-    man.local (* keep local as opposed to IdentitySpec *)
-
-  let combine_assign man (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask): D.t =
+  let combine man state (callee_local: D.t) (lval:lval option) (f: fundec) (args: exp list): D.t =
     (* If we have a function call with assignment
         x = f (e1, ... , ek)
       with a local int variable x on the left, we set it to top *)
-    set_local_int_lval_top man.local lval
+    set_local_int_lval_top state lval
 
-  let special man (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
+  let special man state (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
     (* When calling a special function, and assign the result to some local int variable, we also set it to top. *)
-    set_local_int_lval_top man.local lval
+    set_local_int_lval_top state lval
 
-  let startstate v = D.bot ()
-  let exitstate v = D.top () (* TODO: why is this different from startstate? *)
+  let startstate = D.bot ()
+  let threadenter man state f args = D.top ()
 end
 
 let _ =
-  MCP.register_analysis (module Spec : MCPSpec)
+  MCPRegistry.registered_simplified_analysis (module Spec : SimplifiedSpec)
diff --git a/src/analyses/tutorials/signs.ml b/src/analyses/tutorials/signs.ml
index 06412d6201..92547859cf 100644
--- a/src/analyses/tutorials/signs.ml
+++ b/src/analyses/tutorials/signs.ml
@@ -4,6 +4,7 @@
 
 open GoblintCil
 open Analyses
+open SimplifiedAnalysis
 
 module Signs =
 struct
@@ -44,18 +45,20 @@ struct
     | _ -> false
 end
 
-module Spec : Analyses.MCPSpec =
+module Spec : SimplifiedSpec =
 struct
-  let name () = "signs"
+  include SimplifiedAnalysis.DefaultSpec
+
+  let name = "signs"
+  module V = Printable.Unit
+  module G = Lattice.Unit
 
   (* Map of integers variables to our signs lattice. *)
   module D = MapDomain.MapBot (Basetype.Variables) (SL)
-  include Analyses.ValueContexts(D)
+  module C = D
 
-  let startstate v = D.bot ()
-  let exitstate = startstate
-
-  include Analyses.IdentitySpec
+  let startstate = D.bot ()
+  let startcontext = D.bot ()
 
   (* This should now evaluate expressions. *)
   let eval (d: D.t) (exp: exp): SL.t = match exp with
@@ -67,8 +70,7 @@ struct
 
   (* Transfer functions: we only implement assignments here.
    * You can leave this code alone... *)
-  let assign man (lval:lval) (rval:exp) : D.t =
-    let d = man.local in
+  let assign man d (lval:lval) (rval:exp) : D.t =
     match lval with
     | (Var x, NoOffset) when not x.vaddrof -> D.add x (eval d rval) d
     | _ -> D.top ()
@@ -82,14 +84,17 @@ struct
   (* We should now provide this information to Goblint. Assertions are integer expressions,
    * so we implement here a response to EvalInt queries.
    * You should definitely leave this alone... *)
-  let query man (type a) (q: a Queries.t): a Queries.result =
+  let query man state (type a) (q: a Queries.t): a Queries.result =
     let open Queries in
     match q with
-    | EvalInt e when assert_holds man.local e ->
+    | EvalInt e when assert_holds state e ->
       let ik = Cilfacade.get_ikind_exp e in
       ID.of_bool ik true
     | _ -> Result.top q
+
+  let context man ((state: D.t), _) f callee_state = state
+  let threadenter man state f args = state
 end
 
 let _ =
-  MCP.register_analysis (module Spec : MCPSpec)
+  MCPRegistry.registered_simplified_analysis (module Spec : SimplifiedSpec)
diff --git a/src/analyses/tutorials/simplifiedUnitAnalysis.ml b/src/analyses/tutorials/simplifiedUnitAnalysis.ml
new file mode 100644
index 0000000000..6c4d052aed
--- /dev/null
+++ b/src/analyses/tutorials/simplifiedUnitAnalysis.ml
@@ -0,0 +1,23 @@
+(** Simplest possible analysis with unit domain ([simplifiedUnit]). *)
+
+open GoblintCil
+open SimplifiedAnalysis
+
+module Spec : SimplifiedSpec =
+struct
+  include SimplifiedAnalysis.DefaultSpec
+
+  let name = "simplifiedUnit"
+  module V = Printable.Unit
+  module G = Lattice.Unit
+  module D = Lattice.Unit
+  module C = Printable.Unit
+
+  let startstate = D.bot ()
+  let startcontext = ()
+  let context man (_, c) f callee_state = c
+  let threadenter man state f args = D.top ()
+end
+
+let _ =
+  MCPRegistry.registered_simplified_analysis (module Spec : SimplifiedSpec)
diff --git a/src/analyses/tutorials/solution/signsExtendSol.ml b/src/analyses/tutorials/solution/signsExtendSol.ml
index 04ed920437..36cdf53891 100644
--- a/src/analyses/tutorials/solution/signsExtendSol.ml
+++ b/src/analyses/tutorials/solution/signsExtendSol.ml
@@ -4,6 +4,7 @@
 
 open GoblintCil
 open Analyses
+open SimplifiedAnalysis
 
 module Signs =
 struct
@@ -46,18 +47,20 @@ struct
     for_all (fun x -> for_all (fun y -> Signs.lt x y) y) x
 end
 
-module Spec : Analyses.MCPSpec =
+module Spec : SimplifiedSpec =
 struct
-  let name () = "signsExtendSol"
+  include SimplifiedAnalysis.DefaultSpec
+
+  let name = "signsExtendSol"
+  module V = Printable.Unit
+  module G = Lattice.Unit
 
   (* Map of integers variables to our signs lattice. *)
   module D = MapDomain.MapBot (Basetype.Variables) (SL)
-  include Analyses.ValueContexts(D)
-
-  let startstate v = D.bot ()
-  let exitstate = startstate
+  module C = D
 
-  include Analyses.IdentitySpec
+  let startstate = D.bot ()
+  let startcontext = D.bot ()
 
   (* This should now evaluate expressions. *)
   let eval (d: D.t) (exp: exp): SL.t = match exp with
@@ -69,8 +72,7 @@ struct
 
   (* Transfer functions: we only implement assignments here.
    * You can leave this code alone... *)
-  let assign man (lval:lval) (rval:exp) : D.t =
-    let d = man.local in
+  let assign man d (lval:lval) (rval:exp) : D.t =
     match lval with
     | (Var x, NoOffset) when not x.vaddrof -> D.add x (eval d rval) d
     | _ -> D.top ()
@@ -81,17 +83,17 @@ struct
     | BinOp (Lt, e1, e2, _) -> SL.lt (eval d e1) (eval d e2)
     | _ -> false
 
-  (* We should now provide this information to Goblint. Assertions are integer expressions,
-   * so we implement here a response to EvalInt queries.
-   * You should definitely leave this alone... *)
-  let query man (type a) (q: a Queries.t): a Queries.result =
+  let query man state (type a) (q: a Queries.t): a Queries.result =
     let open Queries in
     match q with
-    | EvalInt e when assert_holds man.local e ->
+    | EvalInt e when assert_holds state e ->
       let ik = Cilfacade.get_ikind_exp e in
       ID.of_bool ik true
     | _ -> Result.top q
+
+  let context man ((state: D.t), _) f callee_state = state
+  let threadenter man state f args = state
 end
 
 let _ =
-  MCP.register_analysis (module Spec : MCPSpec)
+  MCPRegistry.registered_simplified_analysis (module Spec : SimplifiedSpec)
diff --git a/src/analyses/tutorials/solution/signsSol.ml b/src/analyses/tutorials/solution/signsSol.ml
index d757e308d3..d7cafdca4c 100644
--- a/src/analyses/tutorials/solution/signsSol.ml
+++ b/src/analyses/tutorials/solution/signsSol.ml
@@ -4,6 +4,7 @@
 
 open GoblintCil
 open Analyses
+open SimplifiedAnalysis
 
 module Signs =
 struct
@@ -44,18 +45,20 @@ struct
     | _ -> false
 end
 
-module Spec : Analyses.MCPSpec =
+module Spec : SimplifiedSpec =
 struct
-  let name () = "signsSol"
+  include SimplifiedAnalysis.DefaultSpec
+
+  let name = "signsSol"
+  module V = Printable.Unit
+  module G = Lattice.Unit
 
   (* Map of integers variables to our signs lattice. *)
   module D = MapDomain.MapBot (Basetype.Variables) (SL)
-  include Analyses.ValueContexts(D)
-
-  let startstate v = D.bot ()
-  let exitstate = startstate
+  module C = D
 
-  include Analyses.IdentitySpec
+  let startstate = D.bot ()
+  let startcontext = D.bot ()
 
   (* This should now evaluate expressions. *)
   let eval (d: D.t) (exp: exp): SL.t = match exp with
@@ -67,8 +70,7 @@ struct
 
   (* Transfer functions: we only implement assignments here.
    * You can leave this code alone... *)
-  let assign man (lval:lval) (rval:exp) : D.t =
-    let d = man.local in
+  let assign man d (lval:lval) (rval:exp) : D.t =
     match lval with
     | (Var x, NoOffset) when not x.vaddrof -> D.add x (eval d rval) d
     | _ -> D.top ()
@@ -79,17 +81,17 @@ struct
     | BinOp (Lt, e1, e2, _) -> SL.lt (eval d e1) (eval d e2)
     | _ -> false
 
-  (* We should now provide this information to Goblint. Assertions are integer expressions,
-   * so we implement here a response to EvalInt queries.
-   * You should definitely leave this alone... *)
-  let query man (type a) (q: a Queries.t): a Queries.result =
+  let query man state (type a) (q: a Queries.t): a Queries.result =
     let open Queries in
     match q with
-    | EvalInt e when assert_holds man.local e ->
+    | EvalInt e when assert_holds state e ->
       let ik = Cilfacade.get_ikind_exp e in
       ID.of_bool ik true
     | _ -> Result.top q
+
+  let context man ((state: D.t), _) f callee_state = state
+  let threadenter man state f args = state
 end
 
 let _ =
-  MCP.register_analysis (module Spec : MCPSpec)
+  MCPRegistry.registered_simplified_analysis (module Spec : SimplifiedSpec)
diff --git a/src/analyses/tutorials/solution/taintSol.ml b/src/analyses/tutorials/solution/taintSol.ml
index e2bb65d15d..07c95d5cc5 100644
--- a/src/analyses/tutorials/solution/taintSol.ml
+++ b/src/analyses/tutorials/solution/taintSol.ml
@@ -10,6 +10,7 @@
 
 open GoblintCil
 open Analyses
+open SimplifiedAnalysis
 
 module VarinfoSet = SetDomain.Make(CilType.Varinfo)
 
@@ -21,17 +22,17 @@ let is_source varinfo = Cil.hasAttribute "taint_source" varinfo.vattr
 (** "Fake" variable to handle returning from a function *)
 let return_varinfo = dummyFunDec.svar
 
-module Spec : Analyses.MCPSpec =
+module Spec : SimplifiedSpec =
 struct
-  include Analyses.DefaultSpec
-
-  let name () = "taintSol"
+  let name = "taintSol"
+  module V = Printable.Unit
+  module G = Lattice.Unit
   module D = SetDomain.Make(CilType.Varinfo) (* TODO: Change such that you have a fitting local domain *)
   module C = Printable.Unit
 
   (* We are context insensitive in this analysis *)
-  let context man _ _ = ()
-  let startcontext () = ()
+  let context man state f callee_state = ()
+  let startcontext = ()
 
 
   (** Determines whether an expression [e] is tainted, given a [state]. *)
@@ -60,8 +61,10 @@ struct
   (* transfer functions *)
 
   (** Handles assignment of [rval] to [lval]. *)
-  let assign man (lval:lval) (rval:exp) : D.t =
-    let state = man.local in
+  let query man state (type a) (q: a Queries.t): a Queries.result =
+    Queries.Result.top q
+
+  let assign man state (lval:lval) (rval:exp) : D.t =
     match lval with
     | Var v,_ ->
       (* TODO: Check whether rval is tainted, handle assignment to v accordingly *)
@@ -72,15 +75,14 @@ struct
     | _ -> state
 
   (** Handles conditional branching yielding truth value [tv]. *)
-  let branch man (exp:exp) (tv:bool) : D.t =
+  let branch man state (exp:exp) (tv:bool) : D.t =
     (* Nothing needs to be done *)
-    man.local
+    state
 
   (** For a call to a _special_ function f "lval = f(args)" or "f(args)",
       computes the caller state after the function call.
       For this analysis, source and sink functions will be considered _special_ and have to be treated here. *)
-  let special man (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
-    let caller_state = man.local in
+  let special man caller_state (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
     (* TODO: Check if f is a sink / source and handle it appropriately *)
     (* To warn about a potential issue in the code, use M.warn. *)
     if is_source f then
@@ -105,13 +107,12 @@ struct
 
   (** Handles going from start node of function [f] into the function body of [f].
       Meant to handle e.g. initialization of local variables. *)
-  let body man (f:fundec) : D.t =
+  let body man state (f:fundec) : D.t =
     (* Nothing needs to be done here, as the (non-formals) locals are initally untainted *)
-    man.local
+    state
 
   (** Handles the [return] statement, i.e. "return exp" or "return", in function [f]. *)
-  let return man (exp:exp option) (f:fundec) : D.t =
-    let state = man.local in
+  let return man state (exp:exp option) (f:fundec) : D.t =
     match exp with
     | Some e when is_exp_tainted state e ->
       (* TODO: Record whether a tainted value was returned. *)
@@ -123,8 +124,7 @@ struct
       [enter] returns a caller state, and the initial state of the callee.
       In [enter], the caller state can usually be returned unchanged, as [combine_env] and [combine_assign] (below)
       will compute the caller state after the function call, given the return state of the callee. *)
-  let enter man (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
-    let caller_state = man.local in
+  let enter man caller_state (lval: lval option) (f:fundec) (args:exp list) : D.t =
     (* Create list of (formal, actual_exp)*)
     let zipped = List.combine f.sformals args in
     (* TODO: For the initial callee_state, collect formal parameters where the actual is tainted. *)
@@ -134,21 +134,12 @@ struct
         else ts)
         (D.bot ())
         zipped in
-    (* first component is state of caller, second component is state of callee *)
-    [caller_state, callee_state]
+    callee_state
 
   (** For a function call "lval = f(args)" or "f(args)",
       computes the global environment state of the caller after the call.
       Argument [callee_local] is the state of [f] at its return node. *)
-  let combine_env man (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask: Queries.ask): D.t =
-    (* Nothing needs to be done *)
-    man.local
-
-  (** For a function call "lval = f(args)" or "f(args)",
-      computes the state of the caller after assigning the return value from the call.
-      Argument [callee_local] is the state of [f] at its return node. *)
-  let combine_assign man (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask: Queries.ask): D.t =
-    let caller_state = man.local in
+  let combine man caller_state (callee_local:D.t) (lval:lval option) (f: fundec) (args: exp list): D.t =
     (* TODO: Record whether lval was tainted. *)
     match lval with
     | Some (Var v,_) ->
@@ -158,11 +149,9 @@ struct
     | _ -> caller_state
 
   (* You may leave these alone *)
-  let startstate v = D.bot ()
-  let threadenter man ~multiple lval f args = [D.top ()]
-  let threadspawn man ~multiple lval f args fman = man.local
-  let exitstate  v = D.top ()
+  let startstate = D.bot ()
+  let threadenter man state f args = D.top ()
 end
 
 let _ =
-  MCP.register_analysis (module Spec : MCPSpec)
+  MCPRegistry.registered_simplified_analysis (module Spec : SimplifiedSpec)
diff --git a/src/analyses/tutorials/taint.ml b/src/analyses/tutorials/taint.ml
index aadc2f91ea..992cf310a0 100644
--- a/src/analyses/tutorials/taint.ml
+++ b/src/analyses/tutorials/taint.ml
@@ -10,6 +10,7 @@
 
 open GoblintCil
 open Analyses
+open SimplifiedAnalysis
 
 module VarinfoSet = SetDomain.Make(CilType.Varinfo)
 
@@ -21,17 +22,20 @@ let is_source varinfo = Cil.hasAttribute "taint_source" varinfo.vattr
 (** "Fake" variable to handle returning from a function *)
 let return_varinfo = dummyFunDec.svar
 
-module Spec : Analyses.MCPSpec =
+module Spec : SimplifiedSpec =
 struct
-  include Analyses.DefaultSpec
+  include SimplifiedAnalysis.DefaultSpec
 
-  let name () = "taint"
+  let name = "taint"
+
+  module V = Printable.Unit
+  module G = Lattice.Unit
   module D = Lattice.Unit (* TODO: Change such that you have a fitting local domain *)
   module C = Printable.Unit
 
   (* We are context insensitive in this analysis *)
-  let context man _ _ = ()
-  let startcontext () = ()
+  let context man state f callee_state = ()
+  let startcontext = ()
 
 
   (** Determines whether an expression [e] is tainted, given a [state]. *)
@@ -60,8 +64,7 @@ struct
   (* transfer functions *)
 
   (** Handles assignment of [rval] to [lval]. *)
-  let assign man (lval:lval) (rval:exp) : D.t =
-    let state = man.local in
+  let assign man (state: D.t) (lval:lval) (rval:exp) : D.t =
     match lval with
     | Var v,_ ->
       (* TODO: Check whether rval is tainted, handle assignment to v accordingly *)
@@ -69,41 +72,39 @@ struct
     | _ -> state
 
   (** Handles conditional branching yielding truth value [tv]. *)
-  let branch man (exp:exp) (tv:bool) : D.t =
+  let branch man (state: D.t) (exp:exp) (tv:bool) : D.t =
     (* Nothing needs to be done *)
-    man.local
+    state
 
   (** For a call to a _special_ function f "lval = f(args)" or "f(args)",
       computes the caller state after the function call.
       For this analysis, source and sink functions will be considered _special_ and have to be treated here. *)
-  let special man (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
-    let caller_state = man.local in
+  let special man (caller_state: D.t) (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
     (* TODO: Check if f is a sink / source and handle it appropriately *)
     (* To warn about a potential issue in the code, use M.warn. *)
     caller_state
 
   (** Handles going from start node of function [f] into the function body of [f].
       Meant to handle e.g. initialization of local variables. *)
-  let body man (f:fundec) : D.t =
+  let body man (state: D.t) (f:fundec) : D.t =
     (* Nothing needs to be done here, as the (non-formals) locals are initally untainted *)
-    man.local
+    state
 
   (** Handles the [return] statement, i.e. "return exp" or "return", in function [f]. *)
-  let return man (exp:exp option) (f:fundec) : D.t =
-    let state = man.local in
+  let return man (state: D.t) (exp:exp option) (f:fundec) : D.t =
     match exp with
     | Some e ->
       (* TODO: Record whether a tainted value was returned. *)
       (* Hint: You may use return_varinfo in place of a variable. *)
       state
-    | None -> state
+    | None ->
+      state
 
   (** For a function call "lval = f(args)" or "f(args)",
       [enter] returns a caller state, and the initial state of the callee.
       In [enter], the caller state can usually be returned unchanged, as [combine_env] and [combine_assign] (below)
       will compute the caller state after the function call, given the return state of the callee. *)
-  let enter man (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
-    let caller_state = man.local in
+  let enter man (caller_state: D.t) (lval: lval option) (f:fundec) (args:exp list) : D.t =
     (* Create list of (formal, actual_exp)*)
     let zipped = List.combine f.sformals args in
     (* TODO: For the initial callee_state, collect formal parameters where the actual is tainted. *)
@@ -113,30 +114,19 @@ struct
         else ts)
         (D.bot ())
         zipped in
-    (* first component is state of caller, second component is state of callee *)
-    [caller_state, callee_state]
-
-  (** For a function call "lval = f(args)" or "f(args)",
-      computes the global environment state of the caller after the call.
-      Argument [callee_local] is the state of [f] at its return node. *)
-  let combine_env man (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask: Queries.ask): D.t =
-    (* Nothing needs to be done *)
-    man.local
+    callee_state
 
   (** For a function call "lval = f(args)" or "f(args)",
-      computes the state of the caller after assigning the return value from the call.
+      computes the global environment state of the caller after the call and assigning the return value from the call.
       Argument [callee_local] is the state of [f] at its return node. *)
-  let combine_assign man (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask: Queries.ask): D.t =
-    let caller_state = man.local in
+  let combine man (caller_state: D.t) (callee_local:D.t) (lval:lval option) (f: fundec) (args: exp list): D.t =
     (* TODO: Record whether lval was tainted. *)
     caller_state
 
   (* You may leave these alone *)
-  let startstate v = D.bot ()
-  let threadenter man ~multiple lval f args = [D.top ()]
-  let threadspawn man ~multiple lval f args fman = man.local
-  let exitstate  v = D.top ()
+  let startstate = D.bot ()
+  let threadenter man state f args = D.top ()
 end
 
 let _ =
-  MCP.register_analysis (module Spec : MCPSpec)
+  MCPRegistry.registered_simplified_analysis (module Spec : SimplifiedSpec)
diff --git a/src/framework/simplifiedAnalysis.ml b/src/framework/simplifiedAnalysis.ml
index 3b716371c3..a9d378bcd7 100644
--- a/src/framework/simplifiedAnalysis.ml
+++ b/src/framework/simplifiedAnalysis.ml
@@ -72,3 +72,33 @@ module type SimplifiedSpec = sig
   (** Compute the start state of a new thread starting with the function given by fundec *)
   val threadenter: (G.t, C.t, V.t) man -> D.t -> fundec -> exp list -> D.t
 end
+
+module DefaultSpec =
+struct
+  let query man state (type a) (q: a Queries.t) : a Queries.result =
+    Queries.Result.top q
+
+  let assign man state (lval: lval) (rval: exp) =
+    state
+
+  let branch man state (exp: exp) (tv: bool) =
+    state
+
+  let body man state (f: fundec) =
+    state
+
+  let return man state (exp: exp option) (f: fundec) =
+    state
+
+  let enter man state (lval: lval option) (f: fundec) (args: exp list) =
+    state
+
+  let combine man caller_state callee_local (lval: lval option) (f: fundec) (args: exp list) =
+    callee_local
+
+  let special man state (lval: lval option) (f: varinfo) (args: exp list) =
+    state
+
+  let startcontext = ()
+  let context man (_, c) f callee_state = c
+end
diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml
index 2cbe47dad9..d79fa58141 100644
--- a/src/goblint_lib.ml
+++ b/src/goblint_lib.ml
@@ -154,6 +154,7 @@ module Constants = Constants
 module Signs = Signs
 module Taint = Taint
 module UnitAnalysis = UnitAnalysis
+module SimplifiedUnitAnalysis = SimplifiedUnitAnalysis
 
 module GStoreWidening = GStoreWidening
 module GStoreWideningHelper = GStoreWideningHelper