diff --git a/docs/assets/abstraction.png b/docs/assets/abstraction.png
index b5cc94d3b..8a6f9ff86 100644
Binary files a/docs/assets/abstraction.png and b/docs/assets/abstraction.png differ
diff --git a/docs/make.jl b/docs/make.jl
index 1c9bc203f..16e239b47 100644
--- a/docs/make.jl
+++ b/docs/make.jl
@@ -1,24 +1,40 @@
 using Dionysos
 using Documenter, Literate
 
-const EXAMPLES_DIR = joinpath(@__DIR__, "src", "examples")
+const EXAMPLES_SOLVERS_DIR = joinpath(@__DIR__, "src", "examples", "solvers")
+const EXAMPLES_UTILS_DIR = joinpath(@__DIR__, "src", "examples", "utils")
+
 const REFERENCE_DIR = joinpath(@__DIR__, "src", "reference")
 const OUTPUT_DIR = joinpath(@__DIR__, "src", "generated")
 
-const EXAMPLES = readdir(EXAMPLES_DIR)
+const EXAMPLES_SOLVERS = readdir(EXAMPLES_SOLVERS_DIR)
+const EXAMPLES_UTILS = readdir(EXAMPLES_UTILS_DIR)
 const REFERENCE = readdir(REFERENCE_DIR)
 
-for example in EXAMPLES
-    example_filepath = joinpath(EXAMPLES_DIR, example)
-    Literate.markdown(example_filepath, OUTPUT_DIR)
-    Literate.notebook(example_filepath, OUTPUT_DIR)
-    Literate.script(example_filepath, OUTPUT_DIR)
+function literate_actions(file, output_dir)
+    Literate.markdown(file, output_dir)
+    Literate.notebook(file, output_dir)
+    return Literate.script(file, output_dir)
+end
+
+for example in EXAMPLES_SOLVERS
+    literate_actions(joinpath(EXAMPLES_SOLVERS_DIR, example), OUTPUT_DIR)
+end
+for example in EXAMPLES_UTILS
+    literate_actions(joinpath(EXAMPLES_UTILS_DIR, example), OUTPUT_DIR)
 end
+literate_actions(joinpath(@__DIR__, "src", "examples", "Getting Started.jl"), OUTPUT_DIR)
 
 const _PAGES = [
     "Index" => "index.md",
     "Manual" => ["manual/abstraction-based-control.md", "manual/manual.md"],
-    "Examples" => map(EXAMPLES) do jl_file
+    "Getting Started" => "generated/Getting Started.md",
+    "Solvers" => map(EXAMPLES_SOLVERS) do jl_file
+        # Need `string` as Documenter fails if `name` is a `SubString{String}`.
+        name = string(split(jl_file, ".")[1])
+        return name => "generated/$name.md"
+    end,
+    "Utils" => map(EXAMPLES_UTILS) do jl_file
         # Need `string` as Documenter fails if `name` is a `SubString{String}`.
         name = string(split(jl_file, ".")[1])
         return name => "generated/$name.md"
diff --git a/docs/src/developers/setup.md b/docs/src/developers/setup.md
index b40a94482..021ba5b64 100644
--- a/docs/src/developers/setup.md
+++ b/docs/src/developers/setup.md
@@ -115,12 +115,13 @@ julia> using Revise
 
 If you don't plan to test the examples, comment out the Literate part in `docs/make.jl`:
 ```julila
- 11 #for example in EXAMPLES
- 12 #    example_filepath = joinpath(EXAMPLES_DIR, example)
- 13 #    Literate.markdown(example_filepath, OUTPUT_DIR)
- 14 #    Literate.notebook(example_filepath, OUTPUT_DIR)
- 15 #    Literate.script(example_filepath, OUTPUT_DIR)
- 16 #end
+ 20 # for example in EXAMPLES_SOLVERS
+ 21 #     literate_actions(joinpath(EXAMPLES_SOLVERS_DIR, example), OUTPUT_DIR)
+ 22 # end
+ 23 # for example in EXAMPLES_UTILS
+ 24 #     literate_actions(joinpath(EXAMPLES_UTILS_DIR, example), OUTPUT_DIR)
+ 25 # end
+ 26 # literate_actions(joinpath(@__DIR__, "src", "Getting Started.jl"), OUTPUT_DIR)
 ```
 This will speed up building the documentation quite a lot.
 
diff --git a/docs/src/examples/DC-DC converter.jl b/docs/src/examples/solvers/DC-DC converter.jl
similarity index 77%
rename from docs/src/examples/DC-DC converter.jl
rename to docs/src/examples/solvers/DC-DC converter.jl
index fa87af42f..842e0ed83 100644
--- a/docs/src/examples/DC-DC converter.jl	
+++ b/docs/src/examples/solvers/DC-DC converter.jl	
@@ -1,5 +1,5 @@
 using Test     #src
-# # Example: DC-DC converter
+# # Example: DC-DC converter solved by [Naive abstraction](https://github.com/dionysos-dev/Dionysos.jl/blob/master/docs/src/manual/manual.md#solvers).
 #
 #md # [![Binder](https://mybinder.org/badge_logo.svg)](@__BINDER_ROOT_URL__/generated/DC-DC converter.ipynb)
 #md # [![nbviewer](https://img.shields.io/badge/show-nbviewer-579ACA.svg)](@__NBVIEWER_ROOT_URL__/generated/DC-DC converter.ipynb)
@@ -19,24 +19,13 @@ using Test     #src
 # A_1 = \begin{bmatrix} -\frac{r_l}{x_l} &0 \\ 0 & -\frac{1}{x_c}\frac{1}{r_0+r_c}  \end{bmatrix}, A_2= \begin{bmatrix} -\frac{1}{x_l}\left(r_l+\frac{r_0r_c}{r_0+r_c}\right) & -\frac{1}{x_l}\frac{r_0}{r_0+r_c}  \\ \frac{1}{x_c}\frac{r_0}{r_0+r_c}   & -\frac{1}{x_c}\frac{1}{r_0+r_c}  \end{bmatrix}, b = \begin{bmatrix} \frac{v_s}{x_l}\\0\end{bmatrix}.
 # ```
 # The goal is to design a controller to keep the state of the system in a safety region around the reference desired value, using as input only the switching
-# signal.
-#
-#
-# In order to study the concrete system and its symbolic abstraction in a unified framework, we will solve the problem
-# for the sampled system with a sampling time $\tau$.
-#
-# The abstraction is based on a feedback refinment relation [4,V.2 Definition].
-# Basically, this is equivalent to an alternating simulation relationship with the additional constraint that the input of the
-# concrete and symbolic system preserving the relation must be identical.
-# This allows to easily determine the controller of the concrete system from the abstraction controller by simply adding a quantization step.
-#
-# For the construction of the relations in the abstraction, it is necessary to over-approximate attainable sets of
-# a particular cell. In this example, we consider the used of a growth bound function  [4, VIII.2, VIII.5] which is one of the possible methods to over-approximate
-# attainable sets of a particular cell based on the state reach by its center. Therefore, it is used
-# to compute the relations in the abstraction based on the feedback refinement relation.
+# signal. In order to study the concrete system and its symbolic abstraction in a unified framework, we will solve the problem
+# for the sampled system with a sampling time $\tau$. For the construction of the relations in the abstraction, it is necessary to over-approximate attainable sets of
+# a particular cell. In this example, we consider the use of a growth bound function  [4, VIII.2, VIII.5] which is one of the possible methods to over-approximate
+# attainable sets of a particular cell based on the state reach by its center.
 #
 
-# First, let us import [StaticArrays](https://github.com/JuliaArrays/StaticArrays.jl) and [Plots].
+# First, let us import [StaticArrays](https://github.com/JuliaArrays/StaticArrays.jl) and [Plots](https://github.com/JuliaPlots/Plots.jl).
 
 using StaticArrays, Plots
 
@@ -66,7 +55,7 @@ hu = SVector(1)
 input_grid = DO.GridFree(u0, hu)
 
 using JuMP
-optimizer = MOI.instantiate(AB.SCOTSAbstraction.Optimizer)
+optimizer = MOI.instantiate(AB.NaiveAbstraction.Optimizer)
 MOI.set(optimizer, MOI.RawOptimizerAttribute("concrete_problem"), concrete_problem)
 MOI.set(optimizer, MOI.RawOptimizerAttribute("state_grid"), state_grid)
 MOI.set(optimizer, MOI.RawOptimizerAttribute("input_grid"), input_grid)
diff --git a/docs/src/examples/Gol, Lazar & Belta (2013).jl b/docs/src/examples/solvers/Gol, Lazar & Belta (2013).jl
similarity index 96%
rename from docs/src/examples/Gol, Lazar & Belta (2013).jl
rename to docs/src/examples/solvers/Gol, Lazar & Belta (2013).jl
index 50b1a2fe4..1cc46364f 100644
--- a/docs/src/examples/Gol, Lazar & Belta (2013).jl	
+++ b/docs/src/examples/solvers/Gol, Lazar & Belta (2013).jl	
@@ -1,5 +1,5 @@
 using Test     #src
-# # Example: Gol, Lazar and Belta (2013)
+# # Example: Gol, Lazar and Belta (2013) solved by [Bemporad Morari](https://github.com/dionysos-dev/Dionysos.jl/blob/master/docs/src/manual/manual.md#solvers).
 #
 #md # [![Binder](https://mybinder.org/badge_logo.svg)](@__BINDER_ROOT_URL__/generated/Gol%2C Lazar %26 Belta (2013).ipynb)
 #md # [![nbviewer](https://img.shields.io/badge/show-nbviewer-579ACA.svg)](@__NBVIEWER_ROOT_URL__/generated/Gol%2C Lazar %26 Belta (2013).ipynb)
diff --git a/docs/src/examples/Hierarchical-abstraction.jl b/docs/src/examples/solvers/Hierarchical-abstraction.jl
similarity index 95%
rename from docs/src/examples/Hierarchical-abstraction.jl
rename to docs/src/examples/solvers/Hierarchical-abstraction.jl
index 38fbfab27..17ac1e8c7 100644
--- a/docs/src/examples/Hierarchical-abstraction.jl
+++ b/docs/src/examples/solvers/Hierarchical-abstraction.jl
@@ -1,4 +1,4 @@
-# # Hierarchical-abstraction
+# # Example: Reachability problem solved by [Hierarchical abstraction](https://github.com/dionysos-dev/Dionysos.jl/blob/master/docs/src/manual/manual.md#solvers).
 #
 #md # [![Binder](https://mybinder.org/badge_logo.svg)](@__BINDER_ROOT_URL__/generated/Hierarchical-abstraction.ipynb)
 #md # [![nbviewer](https://img.shields.io/badge/show-nbviewer-579ACA.svg)](@__NBVIEWER_ROOT_URL__/generated/Hierarchical-abstraction.ipynb)
@@ -17,7 +17,7 @@ const PR = DI.Problem
 const OP = DI.Optim
 const AB = OP.Abstraction
 
-include("../../../problems/simple_problem.jl")
+include(joinpath(dirname(dirname(pathof(Dionysos))), "problems", "simple_problem.jl"))
 
 ## specific functions
 function post_image(abstract_system, concrete_system, xpos, u)
@@ -125,11 +125,11 @@ AB.LazyAbstraction.set_optimizer_parameters!(
 )
 
 # Global optimizer parameters
-hx_global = [10.0, 10.0] #[15.0, 15.0]
+hx_global = [10.0, 10.0]
 u0 = SVector(0.0, 0.0)
 hu = SVector(0.5, 0.5)
 Ugrid = DO.GridFree(u0, hu)
-max_iter = 6 # 9
+max_iter = 6
 max_time = 1000
 
 optimizer = MOI.instantiate(AB.HierarchicalAbstraction.Optimizer)
diff --git a/docs/src/examples/Lazy-Ellipsoids-Abstraction.jl b/docs/src/examples/solvers/Lazy-Ellipsoids-Abstraction.jl
similarity index 86%
rename from docs/src/examples/Lazy-Ellipsoids-Abstraction.jl
rename to docs/src/examples/solvers/Lazy-Ellipsoids-Abstraction.jl
index 9588ac907..25ca97298 100644
--- a/docs/src/examples/Lazy-Ellipsoids-Abstraction.jl
+++ b/docs/src/examples/solvers/Lazy-Ellipsoids-Abstraction.jl
@@ -1,3 +1,6 @@
+# # Example: Reachability problem solved by [Lazy ellipsoid abstraction](https://github.com/dionysos-dev/Dionysos.jl/blob/master/docs/src/manual/manual.md#solvers).
+#
+
 using StaticArrays, LinearAlgebra, Random, IntervalArithmetic
 using MathematicalSystems, HybridSystems
 using JuMP, Mosek, MosekTools
@@ -15,7 +18,7 @@ const PR = DI.Problem
 const OP = DI.Optim
 const AB = OP.Abstraction
 
-include("../../../problems/non_linear.jl")
+include(joinpath(dirname(dirname(pathof(Dionysos))), "problems", "non_linear.jl"))
 
 # # First example
 
@@ -95,23 +98,24 @@ fig = plot(;
     ytickfontsize = 10,
     guidefontsize = 16,
     titlefontsize = 14,
+    label = false,
 );
 xlabel!("\$x_1\$");
 ylabel!("\$x_2\$");
 title!("Specifictions and domains");
 
 #Display the concrete domain
-plot!(concrete_system.X; color = :yellow, opacity = 0.5);
+plot!(concrete_system.X; color = :yellow, opacity = 0.5, label = false);
 for obs in concrete_system.obstacles
-    plot!(obs; color = :black)
+    plot!(obs; color = :black, label = false)
 end
 
 #Display the abstract domain
-plot!(abstract_system; arrowsB = false, cost = false);
+plot!(abstract_system; arrowsB = false, cost = false, label = false);
 
 #Display the concrete specifications
-plot!(concrete_problem.initial_set; color = :green);
-plot!(concrete_problem.target_set; color = :red)
+plot!(concrete_problem.initial_set; color = :green, label = false);
+plot!(concrete_problem.target_set; color = :red, label = false)
 
 # # Display the abstraction
 fig = plot(;
diff --git a/docs/src/examples/Lazy-abstraction-reachability.jl b/docs/src/examples/solvers/Lazy-abstraction-reachability.jl
similarity index 85%
rename from docs/src/examples/Lazy-abstraction-reachability.jl
rename to docs/src/examples/solvers/Lazy-abstraction-reachability.jl
index 327eee3fb..e37c56384 100644
--- a/docs/src/examples/Lazy-abstraction-reachability.jl
+++ b/docs/src/examples/solvers/Lazy-abstraction-reachability.jl
@@ -1,4 +1,4 @@
-# # Lazy-abstraction-reachability
+# # Example: Reachability problem solved by [Lazy abstraction](https://github.com/dionysos-dev/Dionysos.jl/blob/master/docs/src/manual/manual.md#solvers).
 #
 #md # [![Binder](https://mybinder.org/badge_logo.svg)](@__BINDER_ROOT_URL__/generated/Lazy-abstraction-reachability.ipynb)
 #md # [![nbviewer](https://img.shields.io/badge/show-nbviewer-579ACA.svg)](@__NBVIEWER_ROOT_URL__/generated/Lazy-abstraction-reachability.ipynb)
@@ -8,19 +8,14 @@
 #
 # In order to study the concrete system and its symbolic abstraction in a unified framework, we will solve the problem
 # for the sampled system with a sampling time $\tau$.
-#
-# The abstraction is based on a feedback refinment relation [1,V.2 Definition].
-# This allows to easily determine the controller of the concrete system from the abstraction controller by simply adding a quantization step.
-#
 # For the construction of the relations in the abstraction, it is necessary to over-approximate attainable sets of
 # a particular cell. In this example, we consider the used of a growth bound function  [1, VIII.2, VIII.5] which is one of the possible methods to over-approximate
-# attainable sets of a particular cell based on the state reach by its center. Therefore, it is used
-# to compute the relations in the abstraction based on the feedback refinement relation.
+# attainable sets of a particular cell based on the state reach by its center. 
 #
 # For this reachability problem, the abstraction controller is built using a solver that lazily builds the abstraction, constructing the abstraction 
 # at the same time as the controller.
 
-# First, let us import [StaticArrays](https://github.com/JuliaArrays/StaticArrays.jl) and [Plots].
+# First, let us import [StaticArrays](https://github.com/JuliaArrays/StaticArrays.jl) and [Plots](https://github.com/JuliaPlots/Plots.jl).
 using StaticArrays, JuMP, Plots
 
 # At this point, we import Dionysos.
@@ -34,7 +29,7 @@ const PR = DI.Problem
 const OP = DI.Optim
 const AB = OP.Abstraction
 
-include("../../../problems/simple_problem.jl")
+include(joinpath(dirname(dirname(pathof(Dionysos))), "problems", "simple_problem.jl"))
 
 ## specific functions
 function post_image(abstract_system, concrete_system, xpos, u)
@@ -126,9 +121,9 @@ AB.LazyAbstraction.set_optimizer!(
     Ugrid,
 )
 
-# Build the state feedback abstraction and solve the optimal control problem using A* algorithm
+# Build the abstraction and solve the optimal control problem using A* algorithm
 using Suppressor
-@suppress begin # this is a workaround to supress the undesired output of SDPA
+@suppress begin
     MOI.optimize!(optimizer)
 end
 
@@ -181,7 +176,13 @@ plot!(cost_control_trajectory; ms = 0.5)
 
 # # Display the abstraction and Lyapunov-like function
 fig = plot(; aspect_ratio = :equal);
-plot!(abstract_system; dims = [1, 2], cost = true, lyap_fun = optimizer.lyap_fun)
+plot!(
+    abstract_system;
+    dims = [1, 2],
+    cost = true,
+    lyap_fun = optimizer.lyap_fun,
+    label = false,
+)
 
 # # Display the Bellman-like value function (heuristic)
 fig = plot(; aspect_ratio = :equal)
@@ -191,12 +192,9 @@ plot!(
     dims = [1, 2],
     cost = true,
     lyap_fun = optimizer.bell_fun,
+    label = false,
 )
 
 # # Display the results of the A* algorithm
 fig = plot(; aspect_ratio = :equal)
 plot!(optimizer.lazy_search_problem)
-
-# ### References
-# 1. G. Reissig, A. Weber and M. Rungger, "Feedback Refinement Relations for the Synthesis of Symbolic Controllers," in IEEE Transactions on Automatic Control, vol. 62, no. 4, pp. 1781-1796.
-# 2. K. J. Aström and R. M. Murray, Feedback systems. Princeton University Press, Princeton, NJ, 2008.
diff --git a/docs/src/examples/Path planning.jl b/docs/src/examples/solvers/Path planning.jl
similarity index 88%
rename from docs/src/examples/Path planning.jl
rename to docs/src/examples/solvers/Path planning.jl
index 32a6d2faf..9e681af68 100644
--- a/docs/src/examples/Path planning.jl	
+++ b/docs/src/examples/solvers/Path planning.jl	
@@ -1,5 +1,5 @@
 using Test     #src
-# # Example: Path planning problem
+# # Example: Path planning problem solved by [Naive abstraction](https://github.com/dionysos-dev/Dionysos.jl/blob/master/docs/src/manual/manual.md#solvers).
 #
 #md # [![Binder](https://mybinder.org/badge_logo.svg)](@__BINDER_ROOT_URL__/generated/Path planning.ipynb)
 #md # [![nbviewer](https://img.shields.io/badge/show-nbviewer-579ACA.svg)](@__NBVIEWER_ROOT_URL__/generated/Path planning.ipynb)
@@ -23,21 +23,14 @@ using Test     #src
 #
 # In order to study the concrete system and its symbolic abstraction in a unified framework, we will solve the problem
 # for the sampled system with a sampling time $\tau$.
-#
-# The abstraction is based on a feedback refinment relation [1,V.2 Definition].
-# Basically, this is equivalent to an alternating simulation relationship with the additional constraint that the input of the
-# concrete and symbolic system preserving the relation must be identical.
-# This allows to easily determine the controller of the concrete system from the abstraction controller by simply adding a quantization step.
-#
 # For the construction of the relations in the abstraction, it is necessary to over-approximate attainable sets of
 # a particular cell. In this example, we consider the used of a growth bound function  [1, VIII.2, VIII.5] which is one of the possible methods to over-approximate
-# attainable sets of a particular cell based on the state reach by its center. Therefore, it is used
-# to compute the relations in the abstraction based on the feedback refinement relation.
+# attainable sets of a particular cell based on the state reach by its center.
 #
-# For this reachability problem, the abstraction controller is built by solving a fixed-point equation which consists in computing the the pre-image
+# For this reachability problem, the abstraction controller is built by solving a fixed-point equation which consists in computing the pre-image
 # of the target set.
 
-# First, let us import [StaticArrays](https://github.com/JuliaArrays/StaticArrays.jl) and [Plots].
+# First, let us import [StaticArrays](https://github.com/JuliaArrays/StaticArrays.jl) and [Plots](https://github.com/JuliaPlots/Plots.jl).
 using StaticArrays, Plots
 
 # At this point, we import Dionysos.
@@ -72,10 +65,10 @@ u0 = SVector(0.0, 0.0);
 h = SVector(0.3, 0.3);
 input_grid = DO.GridFree(u0, h);
 
-# We now solve the optimal control problem with the `Abstraction.SCOTSAbstraction.Optimizer`.
+# We now solve the optimal control problem with the `Abstraction.NaiveAbstraction.Optimizer`.
 
 using JuMP
-optimizer = MOI.instantiate(AB.SCOTSAbstraction.Optimizer)
+optimizer = MOI.instantiate(AB.NaiveAbstraction.Optimizer)
 MOI.set(optimizer, MOI.RawOptimizerAttribute("concrete_problem"), concrete_problem)
 MOI.set(optimizer, MOI.RawOptimizerAttribute("state_grid"), state_grid)
 MOI.set(optimizer, MOI.RawOptimizerAttribute("input_grid"), input_grid)
diff --git a/docs/src/examples/State-feedback Abstraction PWA System.jl b/docs/src/examples/solvers/State-feedback Abstraction PWA System.jl
similarity index 97%
rename from docs/src/examples/State-feedback Abstraction PWA System.jl
rename to docs/src/examples/solvers/State-feedback Abstraction PWA System.jl
index 598a075ad..924761a7b 100644
--- a/docs/src/examples/State-feedback Abstraction PWA System.jl	
+++ b/docs/src/examples/solvers/State-feedback Abstraction PWA System.jl	
@@ -1,5 +1,5 @@
 using Test     #src
-# # Example: Optimal control of a PWA System by State-feedback Abstractions
+# # Example: Optimal control of a PWA System by State-feedback Abstractions solved by [Ellipsoid abstraction](https://github.com/dionysos-dev/Dionysos.jl/blob/master/docs/src/manual/manual.md#solvers).
 #
 #md # [![Binder](https://mybinder.org/badge_logo.svg)](@__BINDER_ROOT_URL__/generated/State-feedback Abstraction: PWA System.ipynb)
 #md # [![nbviewer](https://img.shields.io/badge/show-nbviewer-579ACA.svg)](@__NBVIEWER_ROOT_URL__/generated/State-feedback Abstraction: PWA System.ipynb)
@@ -53,7 +53,8 @@ const OP = DI.Optim
 const AB = OP.Abstraction
 
 lib = CDDLib.Library() # polyhedron lib
-include("../../../problems/pwa_sys.jl")
+
+include(joinpath(dirname(dirname(pathof(Dionysos))), "problems", "pwa_sys.jl"))
 
 # # Problem parameters
 # Notice that in [1] it was used `Wsz = 5` and `Usz = 50`. These, and other values were changed here to speed up the build time of the documentation.
diff --git a/docs/src/examples/Ellipsoids.jl b/docs/src/examples/utils/Ellipsoids.jl
similarity index 100%
rename from docs/src/examples/Ellipsoids.jl
rename to docs/src/examples/utils/Ellipsoids.jl
diff --git a/docs/src/examples/Grid.jl b/docs/src/examples/utils/Grid.jl
similarity index 100%
rename from docs/src/examples/Grid.jl
rename to docs/src/examples/utils/Grid.jl
diff --git a/docs/src/examples/Tree.jl b/docs/src/examples/utils/Tree.jl
similarity index 100%
rename from docs/src/examples/Tree.jl
rename to docs/src/examples/utils/Tree.jl
diff --git a/docs/src/index.md b/docs/src/index.md
index 5955e0c47..d73849085 100644
--- a/docs/src/index.md
+++ b/docs/src/index.md
@@ -24,8 +24,9 @@ Rather than relying on closed-form analysis of a model of the dynamical system,
 
 The documentation is organised as follows.
 * The **Manual** section contains all the useful information to use Dionysos as a user.
+* The **Solvers** section contains a few examples of solving problems with Dionysos. Start with [Getting started](https://dionysos-dev.github.io/Dionysos.jl/dev/generated/Getting%20Started/) if you want to get familiar with Dionysos.
+* The **Utils** section contains some examples of basic Dionysos functions.
 * The **API Reference** sections contains all the functions that we currently use in Dionysos. 
-* The **Examples** section contains a few examples of solving problems with Dionysos. Start with [Getting started](https://dionysos-dev.github.io/Dionysos.jl/dev/generated/Getting%20Started/) if you want to get familiar with Dionysos.
 * The **Developer Docs** section is dedicated to the contributors to Dionysos developement. 
 
  
diff --git a/docs/src/manual/abstraction-based-control.md b/docs/src/manual/abstraction-based-control.md
index 4dc26e8b4..7891a76ee 100644
--- a/docs/src/manual/abstraction-based-control.md
+++ b/docs/src/manual/abstraction-based-control.md
@@ -1,18 +1,16 @@
 # Abstraction-based control
 
-Given a mathematical description of the system dynamics and the specifications describing the desired closed-loop behavior of the system, 
-**abstraction-based control** techniques involve synthesizing a **correct-by-construction** controller through a **systematic** three-step procedure. 
-First, both the original system and the specifications are transposed into an abstract domain, resulting in an abstract system and corresponding abstract specifications. 
-This step generally involves a complete discretization of the state and input spaces, typically with uniform hyperrectangles.
-Next, an abstract controller is synthesized to solve this abstract control problem. Finally, the third step, referred to as the **refinement procedure**, involves deducing a controller for the original control problem from the abstract controller. The value of this approach lies in the substitution of the original system (often an infinite system) with a finite system, which enables it to leverage powerful control tools in the domain of symbolic control. This three steps procedure is illustrated on the following figure.
+Given a mathematical description of the system dynamics and the specifications describing the desired closed-loop behavior of the system, **abstraction-based control** techniques involve synthesizing a **correct-by-construction** controller through a **systematic** three-step procedure.
+First, both the original system and the specifications are transposed into an abstract domain, resulting in an abstract system and corresponding abstract specifications.
+We refer to the original system as the concrete system as opposed to the abstract system.
+Next, an abstract controller is synthesized to solve this abstract control problem. Finally, in the third step, called **concretization** as opposed to **abstraction**, a controller for the original control problem is derived from the abstract controller.
 
-<figure>
-    <center><img
-    src="https://github.com/dionysos-dev/Dionysos.jl/blob/master/docs/assets/abstraction.png?raw=true"
-    alt="Abstraction-based control."></center>
-    <center><figcaption>Abstraction-based control</figcaption></center>
-</figure>
+In practice, the abstract domain is constructed by discretizing the concrete state space of the concrete system into subsets (called **cells**).
+The value of this approach lies in the substitution of the concrete system (often a system with an infinite number of states) with a finite state system, which makes it possible to leverage powerful control tools from the graph-theoretic field, such as Dijkstra or the A-star algorithm.
+This three steps procedure is illustrated on the following figure.
+
+![Abstraction-based control.](https://github.com/dionysos-dev/Dionysos.jl/blob/master/docs/assets/abstraction.png?raw=true)
 
 Although this approach offers a safety-critical framework, it suffers from the curse of dimensionality due to the exponential growth of the number of states with respect to the dimension.
 In order to render these techniques practical, it is necessary to construct **smart abstractions**, i.e., they differ from classical techniques in that the partitioning is designed smartly, using optimization-based design techniques, and computed iteratively, unlike the classical approach which uses an a priori defined approach, sub-optimal and subject to the curse of dimensionality.
-To this end, we introduce solvers called **lazy solvers** (i.e. postponing heavier numerical operations) that co-design the abstraction and the controller to reduce the computed part of the abstraction.
\ No newline at end of file
+To this end, we propose solvers called **lazy solvers** (i.e. postponing heavier numerical operations) that co-design the abstraction and the controller to reduce the computed part of the abstraction.
\ No newline at end of file
diff --git a/docs/src/manual/manual.md b/docs/src/manual/manual.md
index 6e9f8c004..b60e10ba6 100644
--- a/docs/src/manual/manual.md
+++ b/docs/src/manual/manual.md
@@ -1,11 +1,11 @@
-# Standard form problem
+# Overview
 
 Dionysos aims to design a controller for a system $\mathcal{S}$ so that the closed-loop system satisfies the specification $\Sigma$ where:
 * the system $\mathcal{S}$ is specified by [`MathematicalSystems`](https://juliareach.github.io/MathematicalSystems.jl/latest/lib/types/#MathematicalSystems.AbstractSystem) or [`HybridSystems`](https://blegat.github.io/HybridSystems.jl/stable/lib/types/#HybridSystems.AbstractHybridSystem) objects;
 * the specification $\Sigma$ is specified by [`ProblemType`](https://dionysos-dev.github.io/Dionysos.jl/dev/reference/Problem/#Dionysos.Problem.ProblemType) objects;
 * the solver $\mathcal{O}$ implementents the abstract type [`AbstractOptimizer`](https://jump.dev/MathOptInterface.jl/stable/reference/models/#MathOptInterface.AbstractOptimizer) of [`MathOptInterface`](https://github.com/jump-dev/MathOptInterface.jl).
 
-So a control problem $(\mathcal{S},\Sigma)$ can be addressed by a solver $\mathcal{O}$ via the [`JuMP`](https://github.com/jump-dev/JuMP.jl) interface, with Dionysos inheriting JuMP's powerful and practical optimization framework.
+So a control problem $(\mathcal{S},\Sigma)$ can be solved by $\mathcal{O}$ via the [`JuMP`](https://github.com/jump-dev/JuMP.jl) interface, with Dionysos inheriting JuMP's powerful and practical optimization framework.
 
 # Overview of the code structure
 Description of the core of the Dionysos.jl package, the [`src`](https://github.com/dionysos-dev/Dionysos.jl/tree/master/src) folder:
@@ -14,8 +14,8 @@ Description of the core of the Dionysos.jl package, the [`src`](https://github.c
 | :--------------- | :---------- |
 | [`utils`](https://github.com/dionysos-dev/Dionysos.jl/tree/master/src/utils) | Contains useful functions, data structures, classic search algorithms, file management, ... |
 | [`domain`](https://github.com/dionysos-dev/Dionysos.jl/tree/master/src/domain) | Contains structures defining the domain of a system |
-| [`system`](https://github.com/dionysos-dev/Dionysos.jl/tree/master/src/system) | Contains specific systems and controllers |
-| [`problem`](https://github.com/dionysos-dev/Dionysos.jl/tree/master/src/problem) | Contains specifications |
+| [`system`](https://github.com/dionysos-dev/Dionysos.jl/tree/master/src/system) | Contains a description of specific systems |
+| [`problem`](https://github.com/dionysos-dev/Dionysos.jl/tree/master/src/problem) | Contains control problems that can be solved by Dionysos solvers |
 | [`symbolic`](https://github.com/dionysos-dev/Dionysos.jl/tree/master/src/symbolic) | Contains the data structures needed to encode the abstractions |
 | [`optim`](https://github.com/dionysos-dev/Dionysos.jl/tree/master/src/optim) | Contains the solvers |
 
@@ -28,9 +28,9 @@ where $\mathcal{X}$ is the state constraint, $\mathcal{U}$ is the input constrai
 * [`HybridSystems`](https://blegat.github.io/HybridSystems.jl/stable/lib/types/#HybridSystems.AbstractHybridSystem), which extends the class of systems of [`MathematicalSystems`](https://juliareach.github.io/MathematicalSystems.jl/latest/lib/types/#MathematicalSystems.AbstractSystem) to hybrid systems.
 
 
-# Specifications
+# Problems
 
-The specification types implemented in Dionysos.jl are:
+The problem types supported in Dionysos.jl are:
 
 | Type         | Description |
 | :--------------- | :---------- |
@@ -41,14 +41,14 @@ Extensions for linear temporal logic (LTL) specifications are currently being im
 
 # Solvers
 
-The following tables summarize the different solver types in abbreviated form. 
+The following tables summarize the different solvers. 
 
 
 **Abstraction-based solver types implemented in Dionysos.jl:**
 
 | Type          | Full vs partial discretization | Partition vs Cover | Shape | Local controller | Abstraction | System | Reference | 
 | :--------------- | :---------- | :---------- | :---------- | :---------- | :---------- | :---------- | :---------- |
-| [`SCOTS`](https://dionysos-dev.github.io/Dionysos.jl/dev/reference/Optim/#Dionysos.Optim.Abstraction.SCOTSAbstraction.Optimizer) | Full | Partition | Hyperrectangle | Piece-wise constant | Non-determinisitic | Continuous-time | [`SCOTS: A Tool for the Synthesis of Symbolic Controllers`](https://dl.acm.org/doi/abs/10.1145/2883817.2883834) |
+| [`Naive abstraction`](https://dionysos-dev.github.io/Dionysos.jl/dev/reference/Optim/#Dionysos.Optim.Abstraction.NaiveAbstraction.Optimizer) | Full | Partition | Hyperrectangle | Piece-wise constant | Non-determinisitic | Continuous-time | [`SCOTS: A Tool for the Synthesis of Symbolic Controllers`](https://dl.acm.org/doi/abs/10.1145/2883817.2883834) |
 | [`Lazy abstraction`](https://dionysos-dev.github.io/Dionysos.jl/dev/reference/Optim/#Dionysos.Optim.Abstraction.LazyAbstraction.Optimizer) | Partial | Partition | Hyperrectangle | Piece-wise constant | Non-determinisitic | Continuous-time | [`Alternating simulation on hierarchical abstractions`](https://ieeexplore.ieee.org/abstract/document/9683448/?casa_token=AXyECYU9FdwAAAAA:ERfvlbkORIbfGLbDd42d2K5K9SLVOjl-8kRs9pfp7lMa4QZEv0W4VgzlP8FshBlxXQF4ZQrDuzk) |
 | [`Hierarchical abstraction`](https://dionysos-dev.github.io/Dionysos.jl/dev/reference/Optim/#Dionysos.Optim.Abstraction.HierarchicalAbstraction.Optimizer) | Partial | Partition | Hyperrectangle | Piece-wise constant | Non-determinisitic | Continuous-time | [`Alternating simulation on hierarchical abstractions`](https://ieeexplore.ieee.org/abstract/document/9683448/?casa_token=AXyECYU9FdwAAAAA:ERfvlbkORIbfGLbDd42d2K5K9SLVOjl-8kRs9pfp7lMa4QZEv0W4VgzlP8FshBlxXQF4ZQrDuzk) |
 | [`Ellipsoid abstraction`](https://dionysos-dev.github.io/Dionysos.jl/dev/reference/Optim/#Dionysos.Optim.Abstraction.EllipsoidsAbstraction.Optimizer) | Full | Cover | Ellipsoid | Piece-wise affine | Determinisitic | Discrete-time affine | [`State-feedback Abstractions for Optimal Control of Piecewise-affine Systems`](https://arxiv.org/abs/2204.00315) |
@@ -64,8 +64,8 @@ The following tables summarize the different solver types in abbreviated form.
 
 **Solver interface**
 
-Each solver is defined by a module which must define the structure [`AbstractOptimizer`](https://jump.dev/MathOptInterface.jl/stable/reference/models/#MathOptInterface.AbstractOptimizer) and implement the [`Optimize!`](https://jump.dev/MathOptInterface.jl/stable/reference/models/#MathOptInterface.optimize!) function.
-For example, for the SCOTS solver, this structure and function are defined as follows
+Each solver is defined by a module which must implement the abstract type [`AbstractOptimizer`](https://jump.dev/MathOptInterface.jl/stable/reference/models/#MathOptInterface.AbstractOptimizer) and the [`Optimize!`](https://jump.dev/MathOptInterface.jl/stable/reference/models/#MathOptInterface.optimize!) function.
+For example, for the NaiveAbstraction solver, this structure and function are defined as follows
 
 ```julia
 using JuMP
@@ -110,9 +110,9 @@ end
 
 # Running an example
 In this section, we outline how to define and solve a control problem with Dionsysos.
-For an executable version of this example, see [`Example: Path planning problem`](https://dionysos-dev.github.io/Dionysos.jl/dev/generated/Path%20planning/#Example:-Path-planning-problem) in the documentation.
+For an executable version of this example, see [`Solvers: Path planning problem`](https://dionysos-dev.github.io/Dionysos.jl/dev/generated/Path%20planning/#Example:-Path-planning-problem) in the documentation.
 
-First you need to define a control problem, i.e., the system and the specification of the desired closed loop behaviour.
+Define a control problem, i.e., the system and the specification of the desired closed loop behaviour.
 To do this, you can define new ones yourself or directly load an existing benchmark, for example
 
 ```julia
@@ -123,7 +123,7 @@ concrete_system = concrete_problem.system;
 Choose the solver you wish to use
 ```julia
 using JuMP
-optimizer = MOI.instantiate(AB.SCOTSAbstraction.Optimizer)
+optimizer = MOI.instantiate(AB.NaiveAbstraction.Optimizer)
 ```
 
 Define the solver's meta-parameters
@@ -166,7 +166,7 @@ plot!(concrete_system.X; color = :yellow, opacity = 0.5);
 plot!(abstract_system.Xdom; color = :blue, opacity = 0.5);
 plot!(concrete_problem.initial_set; color = :green, opacity = 0.2);
 plot!(concrete_problem.target_set; dims = [1, 2], color = :red, opacity = 0.2);
-plot!(UT.DrawTrajectory(x_traj); ms = 0.5)
+plot!(control_trajectory; ms = 0.5)
 ```
 
 
diff --git a/docs/src/reference/Optim.md b/docs/src/reference/Optim.md
index 9ccec33e0..3fe632b67 100644
--- a/docs/src/reference/Optim.md
+++ b/docs/src/reference/Optim.md
@@ -8,7 +8,7 @@ Dionysos.Optim.Abstraction.LazyAbstraction.Optimizer
 Dionysos.Optim.Abstraction.EllipsoidsAbstraction.Optimizer
 Dionysos.Optim.Abstraction.HierarchicalAbstraction.Optimizer
 Dionysos.Optim.Abstraction.LazyEllipsoidsAbstraction.Optimizer
-Dionysos.Optim.Abstraction.SCOTSAbstraction.Optimizer
+Dionysos.Optim.Abstraction.NaiveAbstraction.Optimizer
 ```
 
 ## Other solvers
diff --git a/src/optim/abstraction/abstraction.jl b/src/optim/abstraction/abstraction.jl
index c10a20cf2..32f3b5ad8 100644
--- a/src/optim/abstraction/abstraction.jl
+++ b/src/optim/abstraction/abstraction.jl
@@ -1,6 +1,6 @@
 module Abstraction
 
-include("SCOTS_abstraction.jl")
+include("naive_abstraction.jl")
 include("lazy_abstraction.jl")
 include("hierarchical_abstraction.jl")
 include("ellipsoids_abstraction.jl")
diff --git a/src/optim/abstraction/SCOTS_abstraction.jl b/src/optim/abstraction/naive_abstraction.jl
similarity index 99%
rename from src/optim/abstraction/SCOTS_abstraction.jl
rename to src/optim/abstraction/naive_abstraction.jl
index a2ee9469d..31cbefa06 100644
--- a/src/optim/abstraction/SCOTS_abstraction.jl
+++ b/src/optim/abstraction/naive_abstraction.jl
@@ -1,6 +1,6 @@
-export SCOTSAbstraction
+export NaiveAbstraction
 
-module SCOTSAbstraction
+module NaiveAbstraction
 
 import Dionysos
 const DI = Dionysos
@@ -15,7 +15,7 @@ using JuMP
 """
     Optimizer{T} <: MOI.AbstractOptimizer
 
-SCOTS abstraction solver
+Naive abstraction solver
 """
 mutable struct Optimizer{T} <: MOI.AbstractOptimizer
     concrete_problem::Union{Nothing, PR.ProblemType}
diff --git a/test/optim/test_SCOTS_reachability.jl b/test/optim/test_NaiveAbstraction_reachability.jl
similarity index 96%
rename from test/optim/test_SCOTS_reachability.jl
rename to test/optim/test_NaiveAbstraction_reachability.jl
index 5c6840fb7..918e7e54c 100644
--- a/test/optim/test_SCOTS_reachability.jl
+++ b/test/optim/test_NaiveAbstraction_reachability.jl
@@ -35,10 +35,10 @@ u0 = SVector(0.0, 0.0)
 h = SVector(0.3, 0.3)
 input_grid = DO.GridFree(u0, h)
 
-# We now solve the optimal control problem with the `Abstraction.SCOTSAbstraction.Optimizer`.
+# We now solve the optimal control problem with the `Abstraction.NaiveAbstraction.Optimizer`.
 
 using JuMP
-optimizer = MOI.instantiate(AB.SCOTSAbstraction.Optimizer)
+optimizer = MOI.instantiate(AB.NaiveAbstraction.Optimizer)
 MOI.set(optimizer, MOI.RawOptimizerAttribute("concrete_problem"), concrete_problem)
 MOI.set(optimizer, MOI.RawOptimizerAttribute("state_grid"), state_grid)
 MOI.set(optimizer, MOI.RawOptimizerAttribute("input_grid"), input_grid)
@@ -50,7 +50,7 @@ abstract_problem = MOI.get(optimizer, MOI.RawOptimizerAttribute("abstract_proble
 abstract_controller = MOI.get(optimizer, MOI.RawOptimizerAttribute("abstract_controller"))
 concrete_controller = MOI.get(optimizer, MOI.RawOptimizerAttribute("concrete_controller"))
 
-@testset "SCOTS reachability" begin
+@testset "NaiveAbstraction reachability" begin
     @test length(abstract_controller.data) == 19400 #src
 end
 
diff --git a/test/optim/test_SCOTS_safety.jl b/test/optim/test_NaiveAbstraction_safety.jl
similarity index 95%
rename from test/optim/test_SCOTS_safety.jl
rename to test/optim/test_NaiveAbstraction_safety.jl
index 0a1348510..c65a3e0cb 100644
--- a/test/optim/test_SCOTS_safety.jl
+++ b/test/optim/test_NaiveAbstraction_safety.jl
@@ -29,7 +29,7 @@ hu = SVector(1)
 input_grid = DO.GridFree(u0, hu)
 
 using JuMP
-optimizer = MOI.instantiate(AB.SCOTSAbstraction.Optimizer)
+optimizer = MOI.instantiate(AB.NaiveAbstraction.Optimizer)
 MOI.set(optimizer, MOI.RawOptimizerAttribute("concrete_problem"), concrete_problem)
 MOI.set(optimizer, MOI.RawOptimizerAttribute("state_grid"), state_grid)
 MOI.set(optimizer, MOI.RawOptimizerAttribute("input_grid"), input_grid)
@@ -38,7 +38,7 @@ MOI.optimize!(optimizer)
 abstract_controller = MOI.get(optimizer, MOI.RawOptimizerAttribute("abstract_controller"))
 concrete_controller = MOI.get(optimizer, MOI.RawOptimizerAttribute("concrete_controller"))
 
-@testset "SCOTS safety" begin
+@testset "NaiveAbstraction safety" begin
     @test length(abstract_controller.data) == 893803 #src
 end
 
diff --git a/test/optim/unit_tests_SCOTS/test_controller.jl b/test/optim/unit_tests_NaiveAbstraction/test_controller.jl
similarity index 92%
rename from test/optim/unit_tests_SCOTS/test_controller.jl
rename to test/optim/unit_tests_NaiveAbstraction/test_controller.jl
index 7c71d1bad..d6c308c5a 100644
--- a/test/optim/unit_tests_SCOTS/test_controller.jl
+++ b/test/optim/unit_tests_NaiveAbstraction/test_controller.jl
@@ -11,7 +11,7 @@ sleep(0.1) # used for good printing
 println("Started test")
 
 @testset "Controller" begin
-    contr = AB.SCOTSAbstraction.NewControllerList()
+    contr = AB.NaiveAbstraction.NewControllerList()
 
     UT.push_new!(contr, (5, 6))
     UT.push_new!(contr, (5, 6))
diff --git a/test/optim/unit_tests_SCOTS/test_controllerreach.jl b/test/optim/unit_tests_NaiveAbstraction/test_controllerreach.jl
similarity index 92%
rename from test/optim/unit_tests_SCOTS/test_controllerreach.jl
rename to test/optim/unit_tests_NaiveAbstraction/test_controllerreach.jl
index 5ffd425b8..3e9a52e6a 100644
--- a/test/optim/unit_tests_SCOTS/test_controllerreach.jl
+++ b/test/optim/unit_tests_NaiveAbstraction/test_controllerreach.jl
@@ -75,8 +75,8 @@ println("Started test")
         push!(targetlist, SY.get_state_by_xpos(symmodel, pos))
     end
 
-    contr = AB.SCOTSAbstraction.NewControllerList()
-    AB.SCOTSAbstraction.compute_controller_reach!(
+    contr = AB.NaiveAbstraction.NewControllerList()
+    AB.NaiveAbstraction.compute_controller_reach!(
         contr,
         symmodel.autom,
         initlist,
@@ -85,14 +85,14 @@ println("Started test")
     @test length(contr) == 412
     if VERSION >= v"1.5"
         function f(autom, initlist, targetlist)
-            contr = AB.SCOTSAbstraction.NewControllerList()
+            contr = AB.NaiveAbstraction.NewControllerList()
             initset, targetset, num_targets_unreachable, current_targets, next_targets =
-                AB.SCOTSAbstraction._data(contr, autom, initlist, targetlist)
+                AB.NaiveAbstraction._data(contr, autom, initlist, targetlist)
             # Preallocates to make sure `_compute_controller_reach` does not need to allocate
             sizehint!(contr.data, 500)
             sizehint!(current_targets, 50)
             sizehint!(next_targets, 200)
-            @allocated AB.SCOTSAbstraction._compute_controller_reach!(
+            @allocated AB.NaiveAbstraction._compute_controller_reach!(
                 contr,
                 autom,
                 initset,
diff --git a/test/optim/unit_tests_SCOTS/test_controllersafe.jl b/test/optim/unit_tests_NaiveAbstraction/test_controllersafe.jl
similarity index 96%
rename from test/optim/unit_tests_SCOTS/test_controllersafe.jl
rename to test/optim/unit_tests_NaiveAbstraction/test_controllersafe.jl
index c07fd41f2..b6137f9a7 100644
--- a/test/optim/unit_tests_SCOTS/test_controllersafe.jl
+++ b/test/optim/unit_tests_NaiveAbstraction/test_controllersafe.jl
@@ -74,8 +74,8 @@ println("Started test")
         push!(safelist, SY.get_state_by_xpos(symmodel, pos))
     end
 
-    contr = AB.SCOTSAbstraction.NewControllerList()
-    AB.SCOTSAbstraction.compute_controller_safe!(contr, symmodel.autom, initlist, safelist)
+    contr = AB.NaiveAbstraction.NewControllerList()
+    AB.NaiveAbstraction.compute_controller_safe!(contr, symmodel.autom, initlist, safelist)
     @test length(contr) == 15043
 
     invlist = Int[]
diff --git a/test/optim/unit_tests_SCOTS/test_fromcontrolsystemgrowth.jl b/test/optim/unit_tests_NaiveAbstraction/test_fromcontrolsystemgrowth.jl
similarity index 100%
rename from test/optim/unit_tests_SCOTS/test_fromcontrolsystemgrowth.jl
rename to test/optim/unit_tests_NaiveAbstraction/test_fromcontrolsystemgrowth.jl
diff --git a/test/optim/unit_tests_SCOTS/test_fromcontrolsystemlinearized.jl b/test/optim/unit_tests_NaiveAbstraction/test_fromcontrolsystemlinearized.jl
similarity index 100%
rename from test/optim/unit_tests_SCOTS/test_fromcontrolsystemlinearized.jl
rename to test/optim/unit_tests_NaiveAbstraction/test_fromcontrolsystemlinearized.jl
diff --git a/test/runtests.jl b/test/runtests.jl
index c115dac47..aff17d61b 100644
--- a/test/runtests.jl
+++ b/test/runtests.jl
@@ -23,13 +23,13 @@ include("./symbolic/test_ellipsoidal_transitions.jl")
 
 include("./problem/test_problems.jl")
 
-include("./optim/unit_tests_SCOTS/test_controller.jl")
-include("./optim/unit_tests_SCOTS/test_controllerreach.jl")
-include("./optim/unit_tests_SCOTS/test_controllersafe.jl")
-include("./optim/unit_tests_SCOTS/test_fromcontrolsystemgrowth.jl")
-include("./optim/unit_tests_SCOTS/test_fromcontrolsystemlinearized.jl")
-include("./optim/test_SCOTS_safety.jl")
-include("./optim/test_SCOTS_reachability.jl")
+include("./optim/unit_tests_NaiveAbstraction/test_controller.jl")
+include("./optim/unit_tests_NaiveAbstraction/test_controllerreach.jl")
+include("./optim/unit_tests_NaiveAbstraction/test_controllersafe.jl")
+include("./optim/unit_tests_NaiveAbstraction/test_fromcontrolsystemgrowth.jl")
+include("./optim/unit_tests_NaiveAbstraction/test_fromcontrolsystemlinearized.jl")
+include("./optim/test_NaiveAbstraction_safety.jl")
+include("./optim/test_NaiveAbstraction_reachability.jl")
 include("./optim/test_lazy_abstraction.jl")
 include("./optim/test_ellipsoids_abstraction.jl")
 include("./optim/test_lazy_ellipsoids_abstraction.jl")