diff --git a/src/ReachSets/Properties/IntersectionProperty.jl b/src/Properties/IntersectionProperty.jl
similarity index 100%
rename from src/ReachSets/Properties/IntersectionProperty.jl
rename to src/Properties/IntersectionProperty.jl
diff --git a/src/ReachSets/Properties/LinearConstraintProperty.jl b/src/Properties/LinearConstraintProperty.jl
similarity index 100%
rename from src/ReachSets/Properties/LinearConstraintProperty.jl
rename to src/Properties/LinearConstraintProperty.jl
diff --git a/src/Properties/Properties.jl b/src/Properties/Properties.jl
new file mode 100644
index 00000000..6b828381
--- /dev/null
+++ b/src/Properties/Properties.jl
@@ -0,0 +1,26 @@
+__precompile__()
+"""
+Module for defining and checking properties.
+"""
+module Properties
+
+using LazySets
+
+# ==============================
+# Property struct and evaluation
+# ==============================
+include("Property.jl")
+export Property,
+       check_property
+
+include("LinearConstraintProperty.jl")
+export LinearConstraintProperty,
+       Clause
+
+include("IntersectionProperty.jl")
+export IntersectionProperty
+
+include("SubsetProperty.jl")
+export SubsetProperty
+
+end # module
diff --git a/src/ReachSets/Properties/Property.jl b/src/Properties/Property.jl
similarity index 100%
rename from src/ReachSets/Properties/Property.jl
rename to src/Properties/Property.jl
diff --git a/src/ReachSets/Properties/SubsetProperty.jl b/src/Properties/SubsetProperty.jl
similarity index 100%
rename from src/ReachSets/Properties/SubsetProperty.jl
rename to src/Properties/SubsetProperty.jl
diff --git a/src/ReachSets/Properties/CheckSolution.jl b/src/ReachSets/CheckSolution.jl
similarity index 100%
rename from src/ReachSets/Properties/CheckSolution.jl
rename to src/ReachSets/CheckSolution.jl
diff --git a/src/ReachSets/ContinuousPost/BFFPSV18/check_property.jl b/src/ReachSets/ContinuousPost/BFFPSV18/check_property.jl
index 70197837..0fd16c88 100644
--- a/src/ReachSets/ContinuousPost/BFFPSV18/check_property.jl
+++ b/src/ReachSets/ContinuousPost/BFFPSV18/check_property.jl
@@ -1,4 +1,5 @@
-import LazySets.CacheMinkowskiSum
+using LazySets: CacheMinkowskiSum
+import ..Properties: check_property
 
 """
     check_property(S, property, options)
diff --git a/src/ReachSets/ReachSets.jl b/src/ReachSets/ReachSets.jl
index c5596d61..d937e411 100644
--- a/src/ReachSets/ReachSets.jl
+++ b/src/ReachSets/ReachSets.jl
@@ -80,9 +80,9 @@ AUTHORS:
 """
 module ReachSets
 
-using ..Utils
-using LazySets, MathematicalSystems, HybridSystems
-using Expokit, Optim, ProgressMeter
+using ..Utils, ..Properties
+using LazySets, MathematicalSystems, HybridSystems, Expokit, Optim,
+      ProgressMeter
 
 # fix namespace conflicts with MathematicalSystems
 using LazySets: LinearMap
@@ -107,27 +107,10 @@ include("discretize.jl")
 
 export discretize
 
-# ==============================
-# Property struct and evaluation
-# ==============================
-include("Properties/Property.jl")
-export Property,
-       inout_map_property
-
-include("Properties/LinearConstraintProperty.jl")
-export LinearConstraintProperty,
-       Clause
-
-include("Properties/IntersectionProperty.jl")
-export IntersectionProperty
-
-include("Properties/SubsetProperty.jl")
-export SubsetProperty
-
 # ==========================
 # Property checking results
 # ==========================
-include("Properties/CheckSolution.jl")
+include("CheckSolution.jl")
 
 export CheckSolution
 
@@ -153,7 +136,7 @@ export available_algorithms_check,
 # ====================================================
 # Algorithms to find a threshold for property checking
 # ====================================================
-include("Properties/tune.jl")
+include("tune.jl")
 export tune_δ
 
 # =====================
diff --git a/src/ReachSets/Properties/tune.jl b/src/ReachSets/tune.jl
similarity index 100%
rename from src/ReachSets/Properties/tune.jl
rename to src/ReachSets/tune.jl
diff --git a/src/Reachability.jl b/src/Reachability.jl
index 42b40565..07656c4d 100644
--- a/src/Reachability.jl
+++ b/src/Reachability.jl
@@ -16,11 +16,13 @@ include("Utils/Utils.jl")
 include("Options/dictionary.jl")
 include("Options/validation.jl")
 include("Options/default_options.jl")
+include("Properties/Properties.jl")
 include("ReachSets/ReachSets.jl")
 include("Transformations/Transformations.jl")
 
 @reexport using Reachability.Utils,
                 Reachability.ReachSets,
+                Reachability.Properties,
                 Reachability.Transformations
 
 export project,
diff --git a/test/Properties/unit_tune.jl b/test/Properties/unit_tune.jl
index 52f430c8..fecadf28 100644
--- a/test/Properties/unit_tune.jl
+++ b/test/Properties/unit_tune.jl
@@ -1,4 +1,4 @@
-using Reachability.ReachSets: BFFPSV18
+using Reachability.ReachSets: tune_δ
 
 #===== Projectile model =====
 We test the line plot!(x->x, x->-24*x+375, 0., 50., line=2., color="red", linestyle=:solid, legend=:none)
@@ -17,4 +17,4 @@ algorithm(N, δ) =
           op=BFFPSV18(:δ => δ, :vars => [1, 3], :partition=>[1:2, 3:4])
          ).satisfied
 
-Reachability.tune_δ(algorithm, time_horizon, prec, initial_δ)
+tune_δ(algorithm, time_horizon, prec, initial_δ)
diff --git a/test/ReachSets/unit_discretization.jl b/test/ReachSets/unit_discretization.jl
index 3af9a9ce..77297ea4 100644
--- a/test/ReachSets/unit_discretization.jl
+++ b/test/ReachSets/unit_discretization.jl
@@ -1,5 +1,3 @@
-import Reachability.ReachSets.discretize
-
 let # preventing global scope
     # ===================================================================
     # Discretization of a continuous-time system without input (ZeroSet)
diff --git a/test/Reachability/solve_continuous.jl b/test/Reachability/solve_continuous.jl
index 258a94e4..261a9ec3 100644
--- a/test/Reachability/solve_continuous.jl
+++ b/test/Reachability/solve_continuous.jl
@@ -1,9 +1,6 @@
 # ===============================
 # Test minimal (default) options
 # ===============================
-using Reachability, MathematicalSystems
-using Reachability.ReachSets: BFFPSV18
-using LinearAlgebra, SparseArrays
 
 # linear ODE: x' = Ax
 A = [ 0.0509836  0.168159  0.95246   0.33644
diff --git a/test/Systems/alltests.jl b/test/Systems/alltests.jl
index dff2dba8..c4f24919 100644
--- a/test/Systems/alltests.jl
+++ b/test/Systems/alltests.jl
@@ -1,4 +1,2 @@
-using MathematicalSystems
-
 @time @testset "Systems.NonDeterministicInput" begin include("unit_NonDeterministicInput.jl") end
 @time @testset "Systems.System" begin include("unit_System.jl") end
diff --git a/test/runtests.jl b/test/runtests.jl
index 744f8f2b..adac2556 100644
--- a/test/runtests.jl
+++ b/test/runtests.jl
@@ -1,5 +1,6 @@
 #!/usr/bin/env julia
-using LazySets, Reachability, MathematicalSystems
+using LazySets, Reachability, MathematicalSystems,
+      LinearAlgebra, SparseArrays
 
 # fix namespace conflicts with MathematicalSystems
 import LazySets.LinearMap