diff --git a/.semgrep/stats.yml b/.semgrep/stats.yml
deleted file mode 100644
index c7b29af768..0000000000
--- a/.semgrep/stats.yml
+++ /dev/null
@@ -1,7 +0,0 @@
-rules:
-  - id: stats-time-partial
-    patterns:
-      - pattern: Stats.time $NAME $FUNC $ARG $BADARG ...
-    message: Stats.time measuring only partial, not complete function application (see https://goblint.readthedocs.io/en/latest/developer-guide/profiling/#stats)
-    languages: [ocaml]
-    severity: ERROR
diff --git a/.semgrep/timing.yml b/.semgrep/timing.yml
new file mode 100644
index 0000000000..3da937bd98
--- /dev/null
+++ b/.semgrep/timing.yml
@@ -0,0 +1,16 @@
+rules:
+  - id: cil-stats
+    pattern-either:
+      - pattern: Stats.$FUN
+      - pattern: GoblintCil.Stats.$FUN
+    fix: Timing.$FUN
+    message: use Timing instead
+    languages: [ocaml]
+    severity: ERROR
+
+  - id: timing-time-partial
+    patterns:
+      - pattern: Timing.time $NAME $FUNC $ARG $BADARG ...
+    message: Timing.time measuring only partial, not complete function application (see https://goblint.readthedocs.io/en/latest/developer-guide/profiling/#timing)
+    languages: [ocaml]
+    severity: ERROR
diff --git a/conf/incremental.json b/conf/incremental.json
index f07af41bb9..3d8a20416c 100644
--- a/conf/incremental.json
+++ b/conf/incremental.json
@@ -28,9 +28,11 @@
     "trace": {
       "context": true
     },
-    "debug": true
+    "debug": true,
+    "timing": {
+      "enabled": true
+    }
   },
-  "printstats": true,
   "result": "none",
   "solver": "td3",
   "solvers": {
diff --git a/conf/minimal_incremental.json b/conf/minimal_incremental.json
index 7eb807d3c2..a92468c698 100644
--- a/conf/minimal_incremental.json
+++ b/conf/minimal_incremental.json
@@ -27,9 +27,11 @@
     "trace": {
       "context": true
     },
-    "debug": true
+    "debug": true,
+    "timing": {
+      "enabled": true
+    }
   },
-  "printstats": true,
   "result": "none",
   "solver": "td3",
   "solvers": {
diff --git a/conf/zstd-race.json b/conf/zstd-race.json
index 6465d61719..407e823017 100644
--- a/conf/zstd-race.json
+++ b/conf/zstd-race.json
@@ -75,7 +75,11 @@
       "inlines": false
     }
   },
-  "printstats": true,
+  "dbg": {
+    "timing": {
+      "enabled": true
+    }
+  },
   "warn": {
     "assert": false,
     "behavior": false,
diff --git a/docs/developer-guide/profiling.md b/docs/developer-guide/profiling.md
index 1e9e22d424..df0dde6153 100644
--- a/docs/developer-guide/profiling.md
+++ b/docs/developer-guide/profiling.md
@@ -1,24 +1,34 @@
 # Profiling
 
-## Stats
-`Stats` is an OCaml module from CIL that can be used to profile certain parts of code.
+## Timing
+`Timing` is an OCaml module (based on CIL's `Stats`) that can be used to profile certain parts of code.
 
-Wrap the function call to be profiled with `Stats.time`. For example, replace
+Wrap the function call to be profiled with `Timing.wrap`. For example, replace
 ```ocaml
 f x y z
 ```
 with
 ```ocaml
-Stats.time "mything" (f x y) z
+Timing.wrap "mything" (f x y) z
 ```
 where `mything` should be replaced with a relevant name to be shown in the output.
 Note that all but the last argument are partially applied to `f`.
-The last argument is given separately for `Stats.time` to apply and measure.
+The last argument is given separately for `Timing.wrap` to apply and measure.
 
-Then run Goblint with `--enable printstats` or `-v` (verbose) to see the timing stats under `Timings:`.
+Then run Goblint with `--enable dbg.timing.enabled` or `-v` (verbose) to see the timing stats under `Timings:`.
 
-The timings are automatically presented as a tree which follows the nesting of `Stats.time` calls.
-Unlike [tracing](./debugging.md#tracing), timings cannot be toggled easily, so be considerate of where you leave them after doing the profiling.
+The timings are automatically presented as a tree which follows the nesting of `Timing.wrap` calls.
+Unlike [tracing](./debugging.md#tracing), timings cannot be toggled easily individually, so be considerate of where you leave them after doing the profiling.
+
+### Trace Event Format
+[Trace Event Format (TEF)](https://docs.google.com/document/d/1CvAClvFfyA5R-PhYUmn5OOQtYMH4h6I0nSsKchNAySU/edit) is a simple JSON-based format for profiling data.
+Besides just accumulating timing information, all timed calls are individually recorded, allowing flamegraph-style visualization.
+
+Goblint can produce a TEF file with
+```console
+--enable dbg.timing.enabled --set dbg.timing.tef goblint.timing.json
+```
+Then open `goblint.timing.json` in [Perfetto UI](https://ui.perfetto.dev/).
 
 
 ## perf
diff --git a/dune-project b/dune-project
index fe3069f360..3443890882 100644
--- a/dune-project
+++ b/dune-project
@@ -48,6 +48,8 @@
     arg-complete
     yaml
     uuidm
+    catapult
+    catapult-file
     (conf-gmp (>= 3)) ; only needed transitively, but they don't have lower bound, which is needed on MacOS
     (conf-ruby :with-test)
     (benchmark :with-test) ; TODO: make this optional somehow, (optional) on bench executable doesn't work
diff --git a/goblint.opam b/goblint.opam
index 64e1d1b237..595bf9c5b5 100644
--- a/goblint.opam
+++ b/goblint.opam
@@ -42,6 +42,8 @@ depends: [
   "arg-complete"
   "yaml"
   "uuidm"
+  "catapult"
+  "catapult-file"
   "conf-gmp" {>= "3"}
   "conf-ruby" {with-test}
   "benchmark" {with-test}
@@ -72,7 +74,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 # also remember to generate/adjust goblint.opam.locked!
 available: os-distribution != "alpine" & arch != "arm64"
 pin-depends: [
-  [ "goblint-cil.2.0.0" "git+https://github.com/goblint/cil.git#d4724fe93b0356c611b0b0bd2172210d3f1eeb5b" ]
+  [ "goblint-cil.2.0.0" "git+https://github.com/goblint/cil.git#bfb977b48d6d92e0ecbdab2e04f2576095506107" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
   # TODO: add back after release, only pinned for CI stability
diff --git a/goblint.opam.locked b/goblint.opam.locked
index 3fa2d89d04..b2cb7b4d9d 100644
--- a/goblint.opam.locked
+++ b/goblint.opam.locked
@@ -34,6 +34,8 @@ depends: [
   "bigstringaf" {= "0.8.0"}
   "bos" {= "0.2.1"}
   "camlidl" {= "1.09"}
+  "catapult" {= "0.1.1"}
+  "catapult-file" {= "0.1.1"}
   "cmdliner" {= "1.1.1" & with-doc}
   "conf-autoconf" {= "0.1"}
   "conf-gcc" {= "1.0"}
@@ -122,7 +124,7 @@ available: os-distribution != "alpine" & arch != "arm64"
 pin-depends: [
   [
     "goblint-cil.2.0.0"
-    "git+https://github.com/goblint/cil.git#d4724fe93b0356c611b0b0bd2172210d3f1eeb5b"
+    "git+https://github.com/goblint/cil.git#bfb977b48d6d92e0ecbdab2e04f2576095506107"
   ]
   [
     "apron.v0.9.13"
diff --git a/goblint.opam.template b/goblint.opam.template
index dbe0079bd8..afed06d044 100644
--- a/goblint.opam.template
+++ b/goblint.opam.template
@@ -2,7 +2,7 @@
 # also remember to generate/adjust goblint.opam.locked!
 available: os-distribution != "alpine" & arch != "arm64"
 pin-depends: [
-  [ "goblint-cil.2.0.0" "git+https://github.com/goblint/cil.git#d4724fe93b0356c611b0b0bd2172210d3f1eeb5b" ]
+  [ "goblint-cil.2.0.0" "git+https://github.com/goblint/cil.git#bfb977b48d6d92e0ecbdab2e04f2576095506107" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
   # TODO: add back after release, only pinned for CI stability
diff --git a/scripts/test-incremental-multiple.sh b/scripts/test-incremental-multiple.sh
index 0dee9c117d..7afdadf6a0 100644
--- a/scripts/test-incremental-multiple.sh
+++ b/scripts/test-incremental-multiple.sh
@@ -7,7 +7,7 @@ conf=$base/$test.json
 patch1=$base/${test}_1.patch
 patch2=$base/${test}_2.patch
 
-args="--enable dbg.debug --enable printstats -v"
+args="--enable dbg.debug --enable dbg.timing.enabled -v"
 
 cat $source
 
diff --git a/scripts/test-incremental.sh b/scripts/test-incremental.sh
index 40c244b405..5047390718 100755
--- a/scripts/test-incremental.sh
+++ b/scripts/test-incremental.sh
@@ -11,7 +11,7 @@ source=$base/$test.c
 conf=$base/$test.json
 patch=$base/$test.patch
 
-args="--enable dbg.debug --enable printstats -v --enable allglobs"
+args="--enable dbg.debug --enable dbg.timing.enabled -v --enable allglobs"
 
 ./goblint --conf $conf $args --enable incremental.save $source &> $base/$test.before.log
 
diff --git a/scripts/update_suite.rb b/scripts/update_suite.rb
index 65070303da..5b3efb7e10 100755
--- a/scripts/update_suite.rb
+++ b/scripts/update_suite.rb
@@ -368,7 +368,7 @@ def run_testset (testset, cmd, starttime)
 
   def run
     filename = File.basename(@path)
-    cmd = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --set printstats true --set goblint-dir .goblint-#{@id.sub('/','-')} 2>#{@testset.statsfile}"
+    cmd = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --enable dbg.timing.enabled --set goblint-dir .goblint-#{@id.sub('/','-')} 2>#{@testset.statsfile}"
     starttime = Time.now
     run_testset(@testset, cmd, starttime)
   end
@@ -434,8 +434,8 @@ def create_test_set(lines)
 
   def run
     filename = File.basename(@path)
-    cmd = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --set printstats true --enable incremental.save --set goblint-dir .goblint-#{@id.sub('/','-')}-incr-save 2>#{@testset.statsfile}"
-    cmd_incr = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset_incr.warnfile} --set printstats true --enable incremental.load --set goblint-dir .goblint-#{@id.sub('/','-')}-incr-load 2>#{@testset_incr.statsfile}"
+    cmd = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --enable dbg.timing.enabled --enable incremental.save --set goblint-dir .goblint-#{@id.sub('/','-')}-incr-save 2>#{@testset.statsfile}"
+    cmd_incr = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset_incr.warnfile} --enable dbg.timing.enabled --enable incremental.load --set goblint-dir .goblint-#{@id.sub('/','-')}-incr-load 2>#{@testset_incr.statsfile}"
     starttime = Time.now
     run_testset(@testset_incr, cmd, starttime)
     # apply patch
@@ -478,8 +478,8 @@ def create_test_set(lines)
   end
   def run ()
     filename = File.basename(@path)
-    cmd1 = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --set printstats true --set save_run run --set goblint-dir .goblint-#{@id.sub('/','-')}-run-save 2>#{@testset.statsfile}"
-    cmd2 = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --set printstats true --conf run/config.json --set save_run '' --set load_run run --set goblint-dir .goblint-#{@id.sub('/','-')}-run-load 2>#{@testset.statsfile}"
+    cmd1 = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --enable dbg.timing.enabled --set save_run run --set goblint-dir .goblint-#{@id.sub('/','-')}-run-save 2>#{@testset.statsfile}"
+    cmd2 = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --enable dbg.timing.enabled --conf run/config.json --set save_run '' --set load_run run --set goblint-dir .goblint-#{@id.sub('/','-')}-run-load 2>#{@testset.statsfile}"
     starttime = Time.now
     run_testset(@testset, cmd1, starttime)
     run_testset(@testset, cmd2, starttime)
diff --git a/src/analyses/apron/apronAnalysis.apron.ml b/src/analyses/apron/apronAnalysis.apron.ml
index eab32b3b5b..8b6ecb61a3 100644
--- a/src/analyses/apron/apronAnalysis.apron.ml
+++ b/src/analyses/apron/apronAnalysis.apron.ml
@@ -649,7 +649,7 @@ struct
       RH.map (fun _ -> AD.to_oct) m
     in
     let post_process m =
-      let m = Stats.time "convert" convert m in
+      let m = Timing.wrap "convert" convert m in
       RH.map (fun _ v -> OctApron.marshal v) m
     in
     let results = post_process results in
@@ -661,7 +661,7 @@ struct
     let file = GobConfig.get_string "exp.apron.prec-dump" in
     if file <> "" then begin
       Printf.printf "exp.apron.prec-dump is potentially costly (for domains other than octagons), do not use for performance data!\n";
-      Stats.time "apron.prec-dump" store_data (Fpath.v file)
+      Timing.wrap "apron.prec-dump" store_data (Fpath.v file)
     end;
     Priv.finalize ()
 end
diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml
index a2042a17bc..f1f4fd5482 100644
--- a/src/analyses/basePriv.ml
+++ b/src/analyses/basePriv.ml
@@ -1584,7 +1584,7 @@ struct
   module G = Priv.G
   module V = Priv.V
 
-  let time str f arg = Stats.time "priv" (Stats.time str f) arg
+  let time str f arg = Timing.wrap "priv" (Timing.wrap str f) arg
 
   let startstate = Priv.startstate
   let read_global ask getg st x = time "read_global" (Priv.read_global ask getg st) x
diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml
index 91810887d6..8ff6f372c4 100644
--- a/src/analyses/deadlock.ml
+++ b/src/analyses/deadlock.ml
@@ -108,7 +108,7 @@ struct
         end
       in
 
-      Stats.time "deadlock" (iter_lock LS.empty []) g
+      Timing.wrap ~args:[("lock", `String (Lock.show g))] "deadlock" (iter_lock LS.empty []) g
     | _ -> Queries.Result.top q
 end
 
diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml
index 7e8dc4fcb7..f65ee3e6d9 100644
--- a/src/analyses/raceAnalysis.ml
+++ b/src/analyses/raceAnalysis.ml
@@ -78,7 +78,9 @@ struct
         | `Left g' -> (* accesses *)
           (* ignore (Pretty.printf "WarnGlobal %a\n" CilType.Varinfo.pretty g); *)
           let accs = G.access (ctx.global g) in
-          Stats.time "race" (Access.warn_global safe vulnerable unsafe g') accs
+          let (lv, ty) = g' in
+          let mem_loc_str = Pretty.sprint ~width:max_int (Access.d_memo () (ty, lv)) in
+          Timing.wrap ~args:[("memory location", `String mem_loc_str)] "race" (Access.warn_global safe vulnerable unsafe g') accs
         | `Right _ -> (* vars *)
           ()
       end
diff --git a/src/domains/mapDomain.ml b/src/domains/mapDomain.ml
index 2a1fd1ab6b..b8d0e2ef4d 100644
--- a/src/domains/mapDomain.ml
+++ b/src/domains/mapDomain.ml
@@ -287,7 +287,7 @@ module Timed (M: S) : S with
   type key = M.key and
   type value = M.value =
 struct
-  let time str f arg = GoblintCil.Stats.time (M.name ()) (GoblintCil.Stats.time str f) arg
+  let time str f arg = Timing.wrap (M.name ()) (Timing.wrap str f) arg
 
   (* Printable.S *)
   type t = M.t
diff --git a/src/dune b/src/dune
index 987e56dfba..ec792272b4 100644
--- a/src/dune
+++ b/src/dune
@@ -7,7 +7,7 @@
   (name goblint_lib)
   (public_name goblint.lib)
   (modules :standard \ goblint mainspec privPrecCompare apronPrecCompare messagesCompare)
-  (libraries goblint.sites goblint-cil.all-features batteries.unthreaded qcheck-core.runner sha json-data-encoding jsonrpc cpu arg-complete fpath yaml yaml.unix uuidm
+  (libraries goblint.sites goblint-cil.all-features batteries.unthreaded qcheck-core.runner sha json-data-encoding jsonrpc cpu arg-complete fpath yaml yaml.unix uuidm goblint_timing catapult
     ; Conditionally compile based on whether apron optional dependency is installed or not.
     ; Alternative dependencies seem like the only way to optionally depend on optional dependencies.
     ; See: https://dune.readthedocs.io/en/stable/concepts.html#alternative-dependencies.
diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index 9aa0a6d4e4..1cbe6d61af 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -252,14 +252,9 @@ struct
         BatPrintf.fprintf f "<run>";
         BatPrintf.fprintf f "<parameters>%s</parameters>" Goblintutil.command_line;
         BatPrintf.fprintf f "<statistics>";
-        (* FIXME: This is a super ridiculous hack we needed because BatIO has no way to get the raw channel CIL expects here. *)
-        let name, chn = Filename.open_temp_file "stat" "goblint" in
-        Stats.print chn "";
-        Stdlib.close_out chn;
-        let f_in = BatFile.open_in name in
-        let s = BatIO.read_all f_in in
-        BatIO.close_in f_in;
-        BatPrintf.fprintf f "%s" s;
+        let timing_ppf = BatFormat.formatter_of_out_channel f in
+        Timing.Default.print timing_ppf;
+        Format.pp_print_flush timing_ppf ();
         BatPrintf.fprintf f "</statistics>";
         BatPrintf.fprintf f "<result>\n";
         BatEnum.iter (fun b -> BatPrintf.fprintf f "<file name=\"%s\" path=\"%s\">\n%a</file>\n" (Filename.basename b) b p_funs (SH.find_all file2funs b)) (BatEnum.uniq @@ SH.keys file2funs);
diff --git a/src/framework/cfgTools.ml b/src/framework/cfgTools.ml
index aae9831331..15edb5ee27 100644
--- a/src/framework/cfgTools.ml
+++ b/src/framework/cfgTools.ml
@@ -113,7 +113,7 @@ let computeSCCs (module Cfg: CfgBidir) nodes =
   );
   r
 
-let computeSCCs x = Stats.time "computeSCCs" (computeSCCs x)
+let computeSCCs x = Timing.wrap "computeSCCs" (computeSCCs x)
 
 let rec pretty_edges () = function
   | [] -> Pretty.dprintf ""
@@ -359,7 +359,7 @@ let createCFG (file: file) =
           | ComputedGoto _ ->
             failwith "MyCFG.createCFG: unsupported stmt"
         in
-        Stats.time "handle" (List.iter handle) fd.sallstmts;
+        Timing.wrap ~args:[("function", `String fd.svar.vname)] "handle" (List.iter handle) fd.sallstmts;
 
         if Messages.tracing then Messages.trace "cfg" "Over\n";
 
@@ -436,7 +436,7 @@ let createCFG (file: file) =
           else
             NH.iter (NH.replace node_scc_global) node_scc; (* there's no merge inplace *)
         in
-        Stats.time "iter_connect" iter_connect ();
+        Timing.wrap ~args:[("function", `String fd.svar.vname)] "iter_connect" iter_connect ();
 
         (* Verify that function is now connected *)
         let reachable_return' = find_backwards_reachable ~initial_size:(NH.keys fd_nodes |> BatEnum.hard_count) (module TmpCfg) (Function fd) in
@@ -450,7 +450,7 @@ let createCFG (file: file) =
     ignore (Pretty.eprintf "cfgF (%a), cfgB (%a)\n" GobHashtbl.pretty_statistics (GobHashtbl.magic_stats cfgF) GobHashtbl.pretty_statistics (GobHashtbl.magic_stats cfgB));
   cfgF, cfgB
 
-let createCFG = Stats.time "createCFG" createCFG
+let createCFG = Timing.wrap "createCFG" createCFG
 
 
 let minimizeCFG (fw,bw) =
@@ -580,7 +580,7 @@ let getCFG (file: file) : cfg * cfg =
   let cfgF, cfgB = createCFG file in
   let cfgF, cfgB =
     if get_bool "exp.mincfg" then
-      Stats.time "minimizing the cfg" minimizeCFG (cfgF, cfgB)
+      Timing.wrap "minimizing the cfg" minimizeCFG (cfgF, cfgB)
     else
       (cfgF, cfgB)
   in
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index e1ae56ef1d..16e71037ed 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -690,12 +690,18 @@ struct
 
   let tf (v,c) (e,u) getl sidel getg sideg =
     let old_node = !current_node in
+    let old_fd = Option.map Node.find_fundec old_node |? Cil.dummyFunDec in
+    let new_fd = Node.find_fundec v in
+    if not (CilType.Fundec.equal old_fd new_fd) then
+      Timing.Program.enter new_fd.svar.vname;
     let old_context = !M.current_context in
     current_node := Some u;
     M.current_context := Some (Obj.repr c);
     Fun.protect ~finally:(fun () ->
         current_node := old_node;
-        M.current_context := old_context
+        M.current_context := old_context;
+        if not (CilType.Fundec.equal old_fd new_fd) then
+          Timing.Program.exit new_fd.svar.vname
       ) (fun () ->
         let d       = tf (v,c) (e,u) getl sidel getg sideg in
         d
diff --git a/src/framework/control.ml b/src/framework/control.ml
index 6159f1a936..33e4dec1b9 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -332,7 +332,7 @@ struct
 
     let startstate, more_funs =
       if (get_bool "dbg.verbose") then print_endline ("Initializing "^string_of_int (CfgTools.numGlobals file)^" globals.");
-      Stats.time "global_inits" do_global_inits file
+      Timing.wrap "global_inits" do_global_inits file
     in
 
     let otherfuns = if get_bool "kernel" then otherfuns @ more_funs else otherfuns in
@@ -463,7 +463,7 @@ struct
           if get_bool "dbg.verbose" then
             print_endline ("Solving the constraint system with " ^ get_string "solver" ^ ". Solver statistics are shown every " ^ string_of_int (get_int "dbg.solver-stats-interval") ^ "s or by signal " ^ get_string "dbg.solver-signal" ^ ".");
           Goblintutil.should_warn := get_string "warn_at" = "early" || gobview;
-          let (lh, gh), solver_data = Stats.time "solving" (Slvr.solve entrystates entrystates_global) startvars' in
+          let (lh, gh), solver_data = Timing.wrap "solving" (Slvr.solve entrystates entrystates_global) startvars' in
           if GobConfig.get_bool "incremental.save" then
             Serialize.Cache.(update_data SolverData solver_data);
           if save_run_str <> "" then (
@@ -494,7 +494,7 @@ struct
               Serialize.marshal MCPRegistry.registered_name analyses;
               Serialize.marshal (file, Cabs2cil.environment) cil;
               Serialize.marshal !Messages.Table.messages_list warnings;
-              Serialize.marshal (Stats.top, Gc.quick_stat ()) stats
+              Serialize.marshal (Timing.Default.root, Gc.quick_stat ()) stats
             );
             Goblintutil.(self_signal (signal_of_string (get_string "dbg.solver-signal"))); (* write solver_stats after solving (otherwise no rows if faster than dbg.solver-stats-interval). TODO better way to write solver_stats without terminal output? *)
           );
@@ -645,7 +645,7 @@ struct
       | `Right _ -> (* contexts global *)
         ()
     in
-    Stats.time "warn_global" (GHT.iter warn_global) gh;
+    Timing.wrap "warn_global" (GHT.iter warn_global) gh;
 
     if get_bool "ana.sv-comp.enabled" then
       WResult.write lh gh entrystates;
diff --git a/src/goblint.ml b/src/goblint.ml
index d6f33efe98..343d98fe2d 100644
--- a/src/goblint.ml
+++ b/src/goblint.ml
@@ -9,8 +9,30 @@ open Printf
 let main () =
   try
     Cilfacade.init ();
-    Maingoblint.reset_stats ();
     Maingoblint.parse_arguments ();
+
+    (* Timing. *)
+    Maingoblint.reset_stats ();
+    if get_bool "dbg.timing.enabled" then (
+      let tef_filename = get_string "dbg.timing.tef" in
+      if tef_filename <> "" then
+        Goblint_timing.setup_tef tef_filename;
+      Timing.Default.start {
+        cputime = true;
+        walltime = true;
+        allocated = true;
+        count = true;
+        tef = true;
+      };
+      Timing.Program.start {
+        cputime = false;
+        walltime = false;
+        allocated = false;
+        count = false;
+        tef = true;
+      }
+    );
+
     handle_extraspecials ();
     GoblintDir.init ();
 
@@ -40,20 +62,24 @@ let main () =
       do_stats ();
       do_html_output ();
       do_gobview ();
+      Goblint_timing.teardown_tef ();
       if !verified = Some false then exit 3 (* verifier failed! *)
     )
   with
   | Exit ->
     do_stats ();
+    Goblint_timing.teardown_tef ();
     exit 1
   | Sys.Break -> (* raised on Ctrl-C if `Sys.catch_break true` *)
     do_stats ();
     (* Printexc.print_backtrace BatInnerIO.stderr *)
     eprintf "%s\n" (MessageUtil.colorize ~fd:Unix.stderr ("{RED}Analysis was aborted by SIGINT (Ctrl-C)!"));
+    Goblint_timing.teardown_tef ();
     exit 131 (* same exit code as without `Sys.catch_break true`, otherwise 0 *)
   | Timeout ->
     do_stats ();
     eprintf "%s\n" (MessageUtil.colorize ~fd:Unix.stderr ("{RED}Analysis was aborted because it reached the set timeout of " ^ get_string "dbg.timeout" ^ " or was signalled SIGPROF!"));
+    Goblint_timing.teardown_tef ();
     exit 124
 
 (* We do this since the evaluation order of top-level bindings is not defined, but we want `main` to run after all the other side-effects (e.g. registering analyses/solvers) have happened. *)
diff --git a/src/incremental/compareCFG.ml b/src/incremental/compareCFG.ml
index 96dd47791e..c4663e5266 100644
--- a/src/incremental/compareCFG.ml
+++ b/src/incremental/compareCFG.ml
@@ -115,6 +115,6 @@ let reexamine f1 f2 (same : biDirectionNodeMap) (diffNodes1 : unit NH.t) (module
   NH.to_seq same.node1to2, NH.to_seq_keys diffNodes1
 
 let compareFun (module CfgOld : CfgForward) (module CfgNew : CfgBidir) fun1 fun2 =
-  let same, diff = Stats.time "compare-phase1" (fun () -> compareCfgs (module CfgOld) (module CfgNew) fun1 fun2) () in
-  let unchanged, diffNodes1 = Stats.time "compare-phase2" (fun () -> reexamine fun1 fun2 same diff (module CfgOld) (module CfgNew)) () in
+  let same, diff = Timing.wrap "compare-phase1" (fun () -> compareCfgs (module CfgOld) (module CfgNew) fun1 fun2) () in
+  let unchanged, diffNodes1 = Timing.wrap "compare-phase2" (fun () -> reexamine fun1 fun2 same diff (module CfgOld) (module CfgNew)) () in
   List.of_seq unchanged, List.of_seq diffNodes1
diff --git a/src/incremental/compareCIL.ml b/src/incremental/compareCIL.ml
index 20bb2b7fbe..0d63898f23 100644
--- a/src/incremental/compareCIL.ml
+++ b/src/incremental/compareCIL.ml
@@ -201,4 +201,4 @@ let compareCilFiles ?(eq=eq_glob) (oldAST: file) (newAST: file) =
 (** Given an (optional) equality function between [Cil.global]s, an old and a new [Cil.file], this function computes a [change_info],
     which describes which [global]s are changed, unchanged, removed and added.  *)
 let compareCilFiles ?eq (oldAST: file) (newAST: file) =
-  Stats.time "compareCilFiles" (compareCilFiles ?eq oldAST) newAST
+  Timing.wrap "compareCilFiles" (compareCilFiles ?eq oldAST) newAST
diff --git a/src/maingoblint.ml b/src/maingoblint.ml
index 874c83cfbe..1e9e0125e7 100644
--- a/src/maingoblint.ml
+++ b/src/maingoblint.ml
@@ -90,7 +90,7 @@ let rec option_spec_list: Arg_complete.speclist Lazy.t = lazy (
     complete_option_value !last_complete_option s
   in
   [ "-o"                   , Arg_complete.String (set_string "outfile", Arg_complete.empty), ""
-  ; "-v"                   , Arg_complete.Unit (fun () -> set_bool "dbg.verbose" true; set_bool "printstats" true), ""
+  ; "-v"                   , Arg_complete.Unit (fun () -> set_bool "dbg.verbose" true; set_bool "dbg.timing.enabled" true), ""
   ; "-j"                   , Arg_complete.Int (set_int "jobs", Arg_complete.empty), ""
   ; "-I"                   , Arg_complete.String (set_string "pre.includes[+]", Arg_complete.empty), ""
   ; "-IK"                  , Arg_complete.String (set_string "pre.kernel_includes[+]", Arg_complete.empty), ""
@@ -331,7 +331,7 @@ let preprocess_files () =
       | Unix.WEXITED 0 -> ()
       | process_status -> failwith (GobUnix.string_of_process_status process_status)
     in
-    ProcessPool.run ~jobs:(Goblintutil.jobs ()) ~terminated preprocess_tasks
+    Timing.wrap "preprocess" (ProcessPool.run ~jobs:(Goblintutil.jobs ()) ~terminated) preprocess_tasks
   );
   preprocessed
 
@@ -394,11 +394,12 @@ let preprocess_parse_merge () =
   |> merge_parsed
 
 let do_stats () =
-  if get_bool "printstats" then (
+  if get_bool "dbg.timing.enabled" then (
     print_newline ();
     ignore (Pretty.printf "vars = %d    evals = %d    narrow_reuses = %d\n" !Goblintutil.vars !Goblintutil.evals !Goblintutil.narrow_reuses);
     print_newline ();
-    Stats.print (Messages.get_out "timing" Legacy.stderr) "Timings:\n";
+    print_string "Timings:\n";
+    Timing.Default.print (Format.formatter_of_out_channel @@ Messages.get_out "timing" Legacy.stderr);
     flush_all ()
   )
 
@@ -406,7 +407,8 @@ let reset_stats () =
   Goblintutil.vars := 0;
   Goblintutil.evals := 0;
   Goblintutil.narrow_reuses := 0;
-  Stats.reset SoftwareTimer
+  Timing.Default.reset ();
+  Timing.Program.reset ()
 
 (** Perform the analysis over the merged AST.  *)
 let do_analyze change_info merged_AST =
@@ -449,7 +451,7 @@ let do_analyze change_info merged_AST =
         (* Cilfacade.current_file := ast'; *)
     in
 
-    Stats.time "analysis" (control_analyze merged_AST) funs
+    Timing.wrap "analysis" (control_analyze merged_AST) funs
   )
 
 let do_html_output () =
diff --git a/src/solvers/generic.ml b/src/solvers/generic.ml
index 4ba0b57aed..d8045d5f58 100644
--- a/src/solvers/generic.ml
+++ b/src/solvers/generic.ml
@@ -125,7 +125,7 @@ struct
     (* print_endline "# Solver specific stats"; *)
     !print_solver_stats ();
     print_newline ();
-    (* Stats.print (M.get_out "timing" Legacy.stdout) "Timings:\n"; *)
+    (* Timing.print (M.get_out "timing" Legacy.stdout) "Timings:\n"; *)
     (* Gc.print_stat stdout; (* too verbose, slow and words instead of MB *) *)
     let gc = Goblintutil.print_gc_quick_stat Legacy.stdout in
     print_newline ();
diff --git a/src/solvers/postSolver.ml b/src/solvers/postSolver.ml
index 849bf13304..70687a70ea 100644
--- a/src/solvers/postSolver.ml
+++ b/src/solvers/postSolver.ml
@@ -212,13 +212,13 @@ struct
       if M.tracing then M.trace "postsolver" "one_constraint %a %a\n" S.Var.pretty_trace x S.Dom.pretty rhs;
       PS.one_constraint ~vh ~x ~rhs
     in
-    (GoblintCil.Stats.time "postsolver_iter" (List.iter one_var)) vs;
+    (Timing.wrap "postsolver_iter" (List.iter one_var)) vs;
 
     PS.finalize ~vh ~reachable;
     Goblintutil.postsolving := false
 
   let post xs vs vh =
-    GoblintCil.Stats.time "postsolver" (post xs vs) vh
+    Timing.wrap "postsolver" (post xs vs) vh
 end
 
 (** List of postsolvers. *)
diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml
index 3e2e1efade..20dd88241a 100644
--- a/src/solvers/td3.ml
+++ b/src/solvers/td3.ml
@@ -197,7 +197,7 @@ module WP =
           if tracing then trace "sol" "New Value:%a\n" S.Dom.pretty tmp;
           if tracing then trace "cache" "cache size %d for %a\n" (HM.length l) S.Var.pretty_trace x;
           cache_sizes := HM.length l :: !cache_sizes;
-          if not (Stats.time "S.Dom.equal" (fun () -> S.Dom.equal old tmp) ()) then (
+          if not (Timing.wrap "S.Dom.equal" (fun () -> S.Dom.equal old tmp) ()) then (
             if tracing then trace "sol" "Changed\n";
             update_var_event x old tmp;
             HM.replace rho x tmp;
@@ -778,7 +778,7 @@ module WP =
           List.iter get vs;
           HM.filteri_inplace (fun x _ -> HM.mem visited x) rho
         in
-        Stats.time "restore" restore ();
+        Timing.wrap "restore" restore ();
         if GobConfig.get_bool "dbg.verbose" then ignore @@ Pretty.printf "Solved %d vars. Total of %d vars after restore.\n" !Goblintutil.vars (HM.length rho);
         let avg xs = if List.is_empty !cache_sizes then 0.0 else float_of_int (BatList.sum xs) /. float_of_int (List.length xs) in
         if tracing then trace "cache" "#caches: %d, max: %d, avg: %.2f\n" (List.length !cache_sizes) (List.max !cache_sizes) (avg !cache_sizes);
@@ -861,7 +861,7 @@ module WP =
               Option.may (VS.iter one_var') (HM.find_option side_infl x)
             )
           in
-          (Stats.time "cheap_full_reach" (List.iter one_var')) (vs @ !reluctant_vs);
+          (Timing.wrap "cheap_full_reach" (List.iter one_var')) (vs @ !reluctant_vs);
 
           reachable_and_superstable (* consider superstable reached if it is still reachable: stop recursion (evaluation) and keep from being pruned *)
         else if incr_verify then
diff --git a/src/solvers/topDown_space_cache_term.ml b/src/solvers/topDown_space_cache_term.ml
index 765ec177f2..1ea8c8a8c3 100644
--- a/src/solvers/topDown_space_cache_term.ml
+++ b/src/solvers/topDown_space_cache_term.ml
@@ -181,7 +181,7 @@ module WP =
           in
           List.iter get vs
         in
-        GoblintCil.Stats.time "restore" restore ();
+        Timing.wrap "restore" restore ();
         if (GobConfig.get_bool "dbg.verbose") then ignore @@ Pretty.printf "Solved %d vars. Total of %d vars after restore.\n" !Goblintutil.vars (HM.length rho);
       );
       let avg xs = float_of_int (BatList.sum xs) /. float_of_int (List.length xs) in
diff --git a/src/util/cilfacade.ml b/src/util/cilfacade.ml
index 772bc27c86..ce432eab2a 100644
--- a/src/util/cilfacade.ml
+++ b/src/util/cilfacade.ml
@@ -27,7 +27,9 @@ let init () =
 let current_file = ref dummyFile
 
 let parse fileName =
-  Frontc.parse (Fpath.to_string fileName) ()
+  let fileName_str = Fpath.to_string fileName in
+  let cabs2cil = Timing.wrap ~args:[("file", `String fileName_str)] "FrontC" Frontc.parse fileName_str in
+  Timing.wrap ~args:[("file", `String fileName_str)] "Cabs2cil" cabs2cil ()
 
 let print (fileAST: file) =
   dumpFile defaultCilPrinter stdout "stdout" fileAST
@@ -237,7 +239,7 @@ class addConstructors cons = object
 end
 
 let getMergedAST fileASTs =
-  let merged = Stats.time "mergeCIL"  (Mergecil.merge fileASTs) "stdout" in
+  let merged = Timing.wrap "mergeCIL"  (Mergecil.merge fileASTs) "stdout" in
   if !E.hadErrors then
     E.s (E.error "There were errors during merging\n");
   merged
diff --git a/src/util/options.schema.json b/src/util/options.schema.json
index 36137bc193..548e4203d2 100644
--- a/src/util/options.schema.json
+++ b/src/util/options.schema.json
@@ -29,12 +29,6 @@
       "type": "boolean",
       "default": false
     },
-    "printstats": {
-      "title": "printstats",
-      "description": "Outputs timing information.",
-      "type": "boolean",
-      "default": false
-    },
     "verify": {
       "title": "verify",
       "description":
@@ -1538,6 +1532,25 @@
           "type": "boolean",
           "default": false
         },
+        "timing": {
+          "title": "dbg.timing",
+          "type": "object",
+          "properties": {
+            "enabled": {
+              "title": "dbg.timing.enabled",
+              "description": "Collect and output timing information.",
+              "type": "boolean",
+              "default": false
+            },
+            "tef": {
+              "title": "dbg.timing.tef",
+              "description": "Filename for Trace Event Format (TEF) output. Disabled if empty.",
+              "type": "string",
+              "default": ""
+            }
+          },
+          "additionalProperties": false
+        },
         "trace": {
           "title": "dbg.trace",
           "type": "object",
diff --git a/src/util/processPool.ml b/src/util/processPool.ml
index 506035f040..59eb978ce9 100644
--- a/src/util/processPool.ml
+++ b/src/util/processPool.ml
@@ -22,6 +22,7 @@ let run ~jobs ?(terminated=fun _ _ -> ()) tasks =
           Unix.open_process task.command
       in
       let pid = Unix.process_pid proc in
+      Catapult.Tracing.a_begin ~id:(string_of_int pid) "ProcessPool" ~args:[("command", `String task.command)];
       Hashtbl.replace procs pid (task, proc);
       run tasks
     | [] when Hashtbl.length procs = 0 ->
@@ -35,6 +36,7 @@ let run ~jobs ?(terminated=fun _ _ -> ()) tasks =
           close_in proc_in;
           close_out proc_out;
           Hashtbl.remove procs pid;
+          Catapult.Tracing.a_exit ~id:(string_of_int pid) "ProcessPool";
           terminated task status
         | None -> (* unrelated process *)
           ()
diff --git a/src/util/timing.ml b/src/util/timing.ml
new file mode 100644
index 0000000000..d276a6f2f0
--- /dev/null
+++ b/src/util/timing.ml
@@ -0,0 +1,5 @@
+module Default = Goblint_timing.Make (struct let name = "Default" end)
+
+module Program = Goblint_timing.Make (struct let name = "Program" end)
+
+let wrap = Default.wrap
diff --git a/src/util/timing/dune b/src/util/timing/dune
new file mode 100644
index 0000000000..1a90c9bc12
--- /dev/null
+++ b/src/util/timing/dune
@@ -0,0 +1,6 @@
+(include_subdirs no)
+
+(library
+ (name goblint_timing)
+ (public_name goblint.timing)
+ (libraries catapult catapult-file))
diff --git a/src/util/timing/goblint_timing.ml b/src/util/timing/goblint_timing.ml
new file mode 100644
index 0000000000..c4603f5804
--- /dev/null
+++ b/src/util/timing/goblint_timing.ml
@@ -0,0 +1,220 @@
+include Goblint_timing_intf
+
+(** Dummy options used for initialization before {!S.start} is called. *)
+let dummy_options: options = {
+  cputime = false;
+  walltime = false;
+  allocated = false;
+  count = false;
+  tef = false;
+}
+
+(** TEF process ID for the next {!Make}.
+    We give each timing hierarchy a separate PID in TEF such that they'd be rendered as separate tracks. *)
+let next_tef_pid = ref 0
+
+module Make (Name: Name): S =
+struct
+  let enabled = ref false
+  let options = ref dummy_options
+  let tef_pid =
+    let tef_pid = !next_tef_pid in
+    incr next_tef_pid;
+    tef_pid
+
+  let start options' =
+    options := options';
+    if !options.tef then (
+      (* Override TEF process and thread name for track rendering. *)
+      Catapult.Tracing.emit ~pid:tef_pid "thread_name" ~cat:["__firefox_profiler_hack__"] ~args:[("name", `String Name.name)] Catapult.Event_type.M;
+      (* First event must have category, otherwise Firefox Profiler refuses to open. *)
+      Catapult.Tracing.emit ~pid:tef_pid "process_name" ~args:[("name", `String Name.name)] Catapult.Event_type.M
+    );
+    enabled := true
+
+  let stop () =
+    enabled := false
+
+  let create_tree name =
+    {
+      name = name;
+      cputime = 0.0;
+      walltime = 0.0;
+      allocated = 0.0;
+      count = 0;
+      children = [];
+    }
+
+  let root = create_tree Name.name
+
+  (** A currently active timing frame in the stack. *)
+  type frame = {
+    tree: tree; (** Tree node, where the measurement results will be accumulated. *)
+    start_cputime: float; (** CPU time at the beginning of the frame. *)
+    start_walltime: float; (** Wall time at the beginning of the frame. *)
+    start_allocated: float; (** Allocated memory at the beginning of the frame. *)
+    (* No need for count, because it always gets incremented by 1. *)
+  }
+
+  let current_cputime (): float =
+    let {Unix.tms_utime; tms_stime; tms_cutime; tms_cstime} = Unix.times () in
+    (* Sum CPU time from userspace and kernel, including child processes.
+       This way we account for preprocessor executions. *)
+    tms_utime +. tms_stime +. tms_cutime +. tms_cstime
+
+  let current_walltime (): float =
+    Unix.gettimeofday ()
+
+  let current_allocated = Gc.allocated_bytes
+
+  let create_frame tree =
+    {
+      tree;
+      start_cputime = if !options.cputime then current_cputime () else 0.0;
+      start_walltime = if !options.walltime then current_walltime () else 0.0;
+      start_allocated = if !options.allocated then current_allocated () else 0.0;
+    }
+
+  (** Stack of currently active timing frames. *)
+  let current: frame Stack.t =
+    let current = Stack.create () in
+    Stack.push
+      {
+        tree = root;
+        start_cputime = current_cputime ();
+        start_walltime = current_walltime ();
+        start_allocated = current_allocated ()
+      } current;
+    (* TODO: root frame should actually be created after {!start}, otherwise options are wrong in {!create_frame} *)
+    (* Stack.push (create_frame root) current; *)
+    current
+
+  let reset () =
+    root.children <- [] (* TODO: reset cputime, etc? *)
+
+  let enter ?args name =
+    (* Find the right tree. *)
+    let tree: tree =
+      let {tree; _} = Stack.top current in
+      let rec loop = function
+        | child :: _ when child.name = name -> child
+        | _ :: children' -> loop children'
+        | [] ->
+          (* Not found, create new. *)
+          let tree' = create_tree name in
+          tree.children <- tree' :: tree.children;
+          tree'
+      in
+      loop tree.children
+    in
+    Stack.push (create_frame tree) current;
+    if !options.tef then
+      Catapult.Tracing.begin' ~pid:tef_pid ?args name
+
+  (** Add current frame measurements to tree node accumulators. *)
+  let add_frame_to_tree frame tree =
+    if !options.cputime then (
+      let diff = current_cputime () -. frame.start_cputime in
+      tree.cputime <- tree.cputime +. diff
+    );
+    if !options.walltime then (
+      let diff = current_walltime () -. frame.start_walltime in
+      tree.walltime <- tree.walltime +. diff
+    );
+    if !options.allocated then (
+      let diff = current_allocated () -. frame.start_allocated in
+      tree.allocated <- tree.allocated +. diff
+    );
+    if !options.count then
+      tree.count <- tree.count + 1
+
+  let exit name =
+    let {tree; _} as frame = Stack.pop current in
+    assert (tree.name = name);
+    add_frame_to_tree frame tree;
+    if !options.tef then
+      Catapult.Tracing.exit' ~pid:tef_pid name
+
+  let wrap ?args name f x =
+    enter ?args name;
+    match f x with
+    | r ->
+      exit name;
+      r
+    | exception e ->
+      exit name;
+      raise e
+
+  (* Shortcutting measurement functions to avoid any work when disabled. *)
+
+  let enter ?args name =
+    if !enabled then
+      enter ?args name
+
+  let exit name =
+    if !enabled then
+      exit name
+
+  let wrap ?args name f x =
+    if !enabled then
+      wrap ?args name f x
+    else
+      f x
+
+  (** Root tree with current (entered but not yet exited) frame resources added.
+      This allows printing with in-progress resources also accounted for. *)
+  let root_with_current () =
+    let rec tree_with_current current_rev tree =
+      match current_rev with
+      | frame :: current_rev' when tree == frame.tree ->
+        let tree' = {tree with name = tree.name} in (* new physical copy to avoid mutating original tree *)
+        add_frame_to_tree frame tree';
+        let children = List.map (tree_with_current current_rev') tree.children in
+        {tree' with children}
+      | _ :: current_rev'
+      | ([] as current_rev') ->
+        tree (* no need to recurse, current doesn't go into subtree *)
+    in
+    (* Folding the stack also reverses it such that the root frame is at the beginning. *)
+    let current_rev = Stack.fold (fun acc frame -> frame :: acc) [] current in
+    tree_with_current current_rev root
+
+  let rec pp_tree ppf node =
+    Format.fprintf ppf "@[<v 2>%-25s      " node.name;
+    if !options.cputime then
+      Format.fprintf ppf "%9.3fs" node.cputime;
+    if !options.walltime then
+      Format.fprintf ppf "%10.3fs" node.walltime;
+    if !options.allocated then
+      Format.fprintf ppf "%10.2fMB" (node.allocated /. 1_000_000.0); (* TODO: or should it be 1024-based (MiB)? *)
+    if !options.count then
+      Format.fprintf ppf "%7d×" node.count;
+    (* cut also before first child *)
+    List.iter (Format.fprintf ppf "@,%a" pp_tree) (List.rev node.children);
+    Format.fprintf ppf "@]"
+
+  let pp_header ppf =
+    Format.fprintf ppf "%-25s      " "";
+    if !options.cputime then
+      Format.fprintf ppf "   cputime";
+    if !options.walltime then
+      Format.fprintf ppf "   walltime";
+    if !options.allocated then
+      Format.fprintf ppf "   allocated";
+    if !options.count then
+      Format.fprintf ppf "   count";
+    Format.fprintf ppf "@\n"
+
+  let print ppf =
+    pp_header ppf;
+    pp_tree ppf (root_with_current ());
+    Format.fprintf ppf "@\n"
+end
+
+let setup_tef filename =
+  Catapult_file.set_file filename;
+  Catapult_file.enable ();
+  Catapult_file.setup ()
+
+let teardown_tef () =
+  Catapult_file.teardown ()
diff --git a/src/util/timing/goblint_timing.mli b/src/util/timing/goblint_timing.mli
new file mode 100644
index 0000000000..8fde1cc6cb
--- /dev/null
+++ b/src/util/timing/goblint_timing.mli
@@ -0,0 +1,3 @@
+(** Profiling with custom hierarchical timed sections. *)
+
+include Goblint_timing_intf.Goblint_timing (** @inline *)
diff --git a/src/util/timing/goblint_timing_intf.ml b/src/util/timing/goblint_timing_intf.ml
new file mode 100644
index 0000000000..e41d33d6b8
--- /dev/null
+++ b/src/util/timing/goblint_timing_intf.ml
@@ -0,0 +1,85 @@
+module type Name =
+sig
+  val name: string
+  (** Name of timing hierarchy.
+      Used in {!S.print} and TEF track. *)
+end
+
+(** Timing options. *)
+type options = {
+  cputime: bool; (** Measure CPU time, both userspace and kernel, including child processes. *)
+  walltime: bool; (** Measure wall time. *)
+  allocated: bool; (** Measure allocated memory. *)
+  count: bool; (** Count calls. *)
+  tef: bool; (** Output a TEF track. *)
+}
+
+(** Timing tree node. *)
+type tree = {
+  name: string; (** Name of node. *)
+  mutable cputime: float; (** Accumulated CPU time in seconds. *)
+  mutable walltime: float; (** Accumulated wall time in seconds. *)
+  mutable allocated: float; (** Accumulated allocated memory in bytes. *)
+  mutable count: int; (** Number of repetitions. Only set if {!Timing.countCalls} is true. *)
+  mutable children: tree list; (** Child nodes. *)
+}
+
+(** Timing hierarchy. *)
+module type S =
+sig
+  (** {2 Lifecycle} *)
+
+  val start: options -> unit
+  (** Start timing with options. *)
+
+  val stop: unit -> unit
+  (** Stop timing, but don't reset timing information. *)
+
+  val reset: unit -> unit
+  (** Reset timing information. *)
+
+  (** {2 Measurement} *)
+
+  val enter: ?args:(string * Catapult.Tracing.arg) list -> string -> unit
+  (** [enter name] enters a new nested timed section called [name].
+      @param args custom data for TEF *)
+
+  val exit: string -> unit
+  (** [exit name] exits the current timed section called [name].
+      Sections must be exited in valid nested fashion. *)
+
+  val wrap: ?args:(string * Catapult.Tracing.arg) list -> string -> ('a -> 'b) -> 'a -> 'b
+  (** [wrap name f x] runs [f x] and measures it as a timed section called [name].
+      @param args custom data for TEF *)
+
+  (** {2 Output} *)
+
+  val print: Format.formatter -> unit
+  (** Pretty-print current timing hierarchy. *)
+
+  val root: tree
+  (** Root node of timing tree.
+      Must not be mutated! *)
+end
+
+module type Goblint_timing =
+sig
+  module type Name = Name
+
+  type nonrec options = options
+  type nonrec tree = tree
+
+  module type S = S
+
+  module Make (Name: Name): S
+  (** Make a new timing hierarchy. *)
+
+  val setup_tef: string -> unit
+  (** [setup_tef filename] sets up Trace Event Format (TEF) output to [filename].
+
+      @see <https://ui.perfetto.dev> for Perfetto UI for opening TEF files.
+      @see <https://docs.google.com/document/d/1CvAClvFfyA5R-PhYUmn5OOQtYMH4h6I0nSsKchNAySU/edit> for TEF specification. *)
+
+  val teardown_tef: unit -> unit
+  (** Tear down TEF output. Must be called to correctly terminate the file. *)
+end
diff --git a/src/witness/witness.ml b/src/witness/witness.ml
index f3978a204d..a4caadb72c 100644
--- a/src/witness/witness.ml
+++ b/src/witness/witness.ml
@@ -3,8 +3,6 @@ open Graphml
 open Svcomp
 open GobConfig
 
-module Stats = GoblintCil.Stats
-
 module type WitnessTaskResult = TaskResult with module Arg.Edge = MyARG.InlineEdge
 
 let write_file filename (module Task:Task) (module TaskResult:WitnessTaskResult): unit =
@@ -571,14 +569,14 @@ struct
 
   let write lh gh entrystates =
     let module Task = (val (BatOption.get !task)) in
-    let module TaskResult = (val (Stats.time "determine" (determine_result lh gh entrystates) (module Task))) in
+    let module TaskResult = (val (Timing.wrap "determine" (determine_result lh gh entrystates) (module Task))) in
 
     print_task_result (module TaskResult);
 
     (* TODO: use witness.enabled elsewhere as well *)
     if get_bool "witness.enabled" && (TaskResult.result <> Result.Unknown || get_bool "witness.unknown") then (
       let witness_path = get_string "witness.path" in
-      Stats.time "write" (write_file witness_path (module Task)) (module TaskResult)
+      Timing.wrap "write" (write_file witness_path (module Task)) (module TaskResult)
     )
 
   let write lh gh entrystates =
@@ -587,5 +585,5 @@ struct
     | _ -> write lh gh entrystates
 
   let write lh gh entrystates =
-    Stats.time "witness" (write lh gh) entrystates
+    Timing.wrap "witness" (write lh gh) entrystates
 end
diff --git a/src/witness/witnessUtil.ml b/src/witness/witnessUtil.ml
index 16ec48c548..ad2e4a424b 100644
--- a/src/witness/witnessUtil.ml
+++ b/src/witness/witnessUtil.ml
@@ -134,7 +134,7 @@ struct
     {global_vars}
 
   let parse_cabs (inv: string): (Cabs.expression, string) result =
-    match Frontc.parse_standalone_exp inv with
+    match Timing.wrap "FrontC" Frontc.parse_standalone_exp inv with
     | inv_cabs -> Ok inv_cabs
     | exception (Frontc.ParseError e) ->
       Errormsg.log "\n"; (* CIL prints garbage without \n before *)
@@ -158,7 +158,7 @@ struct
           Cil.useLogicalOperators := old_useLogicalOperators
         ) (fun () ->
           Cil.useLogicalOperators := true;
-          Cabs2cil.convStandaloneExp ~genv ~env inv_cabs
+          Timing.wrap "Cabs2cil" (Cabs2cil.convStandaloneExp ~genv ~env) inv_cabs
         )
     in
 
diff --git a/tests/regression/46-apron2/18-evalint-torture.c b/tests/regression/46-apron2/18-evalint-torture.c
index 37d8d3736a..f869b9305a 100644
--- a/tests/regression/46-apron2/18-evalint-torture.c
+++ b/tests/regression/46-apron2/18-evalint-torture.c
@@ -3,15 +3,15 @@
 
 // Previously using with MustBeEqual, MayBeEqual and MayBeLess queries:
 // Ran in 3.0-3.5s.
-// ./goblint --set ana.activated[+] apron --enable printstats ./tests/regression/46-apron2/18-evalint-torture.c
+// ./goblint --set ana.activated[+] apron --enable dbg.timing.enabled ./tests/regression/46-apron2/18-evalint-torture.c
 
 // Without those queries, but with deep-query:
 // Ran in 2.4-2.7s.
-// ./goblint --set ana.activated[+] apron --enable printstats ./tests/regression/46-apron2/18-evalint-torture.c --enable ana.base.eval.deep-query
+// ./goblint --set ana.activated[+] apron --enable dbg.timing.enabled ./tests/regression/46-apron2/18-evalint-torture.c --enable ana.base.eval.deep-query
 
 // Without those queries and deep-query:
 // Ran in 1.6-1.7s.
-// ./goblint --set ana.activated[+] apron --enable printstats ./tests/regression/46-apron2/18-evalint-torture.c --disable ana.base.eval.deep-query
+// ./goblint --set ana.activated[+] apron --enable dbg.timing.enabled ./tests/regression/46-apron2/18-evalint-torture.c --disable ana.base.eval.deep-query
 
 #include <assert.h>