diff --git a/src/cli/cli.cpp b/src/cli/cli.cpp
index c9e0aa7e6..36b6df27e 100644
--- a/src/cli/cli.cpp
+++ b/src/cli/cli.cpp
@@ -1,4 +1,5 @@
 #include "cli.h"
+#include "entrypoints.h"
 
 #include "../utility/storm.h"
 
@@ -7,6 +8,7 @@
 
 #include "src/utility/storm-version.h"
 
+
 // Includes for the linked libraries and versions header.
 #ifdef STORM_HAVE_INTELTBB
 #	include "tbb/tbb_stddef.h"
@@ -110,7 +112,7 @@ namespace storm {
 					std::cout << "Compiled with CUDA support, but an error occured trying to find CUDA devices." << std::endl;
 				}
 #endif
-                
+
                 // "Compute" the command line argument string with which STORM was invoked.
                 std::stringstream commandStream;
                 for (int i = 1; i < argc; ++i) {
diff --git a/src/utility/storm.h b/src/utility/storm.h
index bb3a0a8a5..19f84b85d 100644
--- a/src/utility/storm.h
+++ b/src/utility/storm.h
@@ -209,22 +209,7 @@ namespace storm {
         return result;
 
     }
-            
-    template<typename ValueType>
-    void verifySparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
-        for (auto const& formula : formulas) {
-            std::cout << std::endl << "Model checking property: " << *formula << " ...";
-            std::unique_ptr<storm::modelchecker::CheckResult> result(verifySparseModel(model, formula));
-            if (result) {
-                std::cout << " done." << std::endl;
-                std::cout << "Result (initial states): ";
-                result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
-                std::cout << *result << std::endl;
-            } else {
-                std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
-            }
-        }
-    }
+
             
 #ifdef STORM_HAVE_CARL
     inline void exportParametricResultToFile(storm::RationalFunction const& result, storm::models::sparse::Dtmc<storm::RationalFunction>::ConstraintCollector const& constraintCollector, std::string const& path) {
@@ -242,39 +227,22 @@ namespace storm {
         std::copy(constraintCollector.getGraphPreservingConstraints().begin(), constraintCollector.getGraphPreservingConstraints().end(), std::ostream_iterator<storm::ArithConstraint<storm::RationalFunction>>(filestream, "\n"));
         filestream.close();
     }
-            
-    template<>
-    inline void verifySparseModel(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
-
-        for (auto const& formula : formulas) {
-            STORM_LOG_THROW(model->getType() == storm::models::ModelType::Dtmc, storm::exceptions::InvalidSettingsException, "Currently parametric verification is only available for DTMCs.");
-            std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
-
-            std::cout << std::endl << "Model checking property: " << *formula << " ...";
-            std::unique_ptr<storm::modelchecker::CheckResult> result;
-
-            storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>> modelchecker(*dtmc);
-            if (modelchecker.canHandle(*formula)) {
-                result = modelchecker.check(*formula);
-            } else {
-                STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The parametric engine currently does not support this property.");
-            }
 
-            if (result) {
-                std::cout << " done." << std::endl;
-                std::cout << "Result (initial states): ";
-                result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(dtmc->getInitialStates()));
-                std::cout << *result << std::endl;
-            } else {
-                std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
-            }
+    template<>
+    inline std::unique_ptr<storm::modelchecker::CheckResult> verifySparseModel(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::shared_ptr<storm::logic::Formula> const& formula) {
+        std::unique_ptr<storm::modelchecker::CheckResult> result;
+        std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
 
-            storm::settings::modules::ParametricSettings const& parametricSettings = storm::settings::parametricSettings();
-            if (parametricSettings.exportResultToFile()) {
-                exportParametricResultToFile(result->asExplicitQuantitativeCheckResult<storm::RationalFunction>()[*dtmc->getInitialStates().begin()], storm::models::sparse::Dtmc<storm::RationalFunction>::ConstraintCollector(*dtmc), parametricSettings.exportResultPath());
-            }
+        storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>> modelchecker(*dtmc);
+        if (modelchecker.canHandle(*formula)) {
+            result = modelchecker.check(*formula);
+        } else {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The parametric engine currently does not support this property.");
         }
+        return result;
     }
+            
+
 #endif
 
     template<storm::dd::DdType DdType>
@@ -304,22 +272,6 @@ namespace storm {
         return result;
     }
 
-    template<storm::dd::DdType DdType>
-    void verifySymbolicModelWithHybridEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
-        for (auto const& formula : formulas) {
-            std::cout << std::endl << "Model checking property: " << *formula << " ...";
-            std::unique_ptr<storm::modelchecker::CheckResult> result(verifySymbolicModelWithHybridEngine(model, formula));
-
-            if (result) {
-                std::cout << " done." << std::endl;
-                std::cout << "Result (initial states): ";
-                result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(model->getReachableStates(), model->getInitialStates()));
-                std::cout << *result << std::endl;
-            } else {
-                std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
-            }
-        }
-    }
 
     template<storm::dd::DdType DdType>
     std::unique_ptr<storm::modelchecker::CheckResult> verifySymbolicModelWithDdEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::shared_ptr<storm::logic::Formula> const& formula) {
@@ -341,76 +293,6 @@ namespace storm {
         }
         return result;
     }
-
-    template<storm::dd::DdType DdType>
-    void verifySymbolicModelWithSymbolicEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
-        for (auto const& formula : formulas) {
-            std::cout << std::endl << "Model checking property: " << *formula << " ...";
-            std::unique_ptr<storm::modelchecker::CheckResult> result(verifySymbolicModelWithDdEngine(model, formula));
-            if (result) {
-                std::cout << " done." << std::endl;
-                std::cout << "Result (initial states): ";
-                result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(model->getReachableStates(), model->getInitialStates()));
-                std::cout << *result << std::endl;
-            } else {
-                std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
-            }
-        }
-    }
-
-
-    template<typename ValueType>
-    void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
-        std::shared_ptr<storm::models::ModelBase> model = buildSymbolicModel<ValueType>(program, formulas);
-        STORM_LOG_THROW(model != nullptr, storm::exceptions::InvalidStateException, "Model could not be constructed for an unknown reason.");
-
-        // Preprocess the model if needed.
-        model = preprocessModel<ValueType>(model, formulas);
-
-        // Print some information about the model.
-        model->printModelInformationToStream(std::cout);
-
-        // Verify the model, if a formula was given.
-        if (!formulas.empty()) {
-            if (model->isSparseModel()) {
-                if(storm::settings::generalSettings().isCounterexampleSet()) {
-                    // If we were requested to generate a counterexample, we now do so for each formula.
-                    for(auto const& formula : formulas) {
-                        generateCounterexample<ValueType>(program, model->as<storm::models::sparse::Model<ValueType>>(), formula);
-                    }
-                } else {
-                    verifySparseModel<ValueType>(model->as<storm::models::sparse::Model<ValueType>>(), formulas);
-                }
-            } else if (model->isSymbolicModel()) {
-                if (storm::settings::generalSettings().getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) {
-                    verifySymbolicModelWithHybridEngine(model->as<storm::models::symbolic::Model<storm::dd::DdType::CUDD>>(), formulas);
-                } else {
-                    verifySymbolicModelWithSymbolicEngine(model->as<storm::models::symbolic::Model<storm::dd::DdType::CUDD>>(), formulas);
-                }
-            } else {
-                STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Invalid input model type.");
-            }
-        }
-    }
-            
-    template<typename ValueType>
-    void buildAndCheckExplicitModel(std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
-        storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings();
-
-        STORM_LOG_THROW(settings.isExplicitSet(), storm::exceptions::InvalidStateException, "Unable to build explicit model without model files.");
-         std::shared_ptr<storm::models::ModelBase> model = buildExplicitModel<ValueType>(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? settings.getStateRewardsFilename() : boost::optional<std::string>(), settings.isTransitionRewardsSet() ? settings.getTransitionRewardsFilename() : boost::optional<std::string>(), settings.isChoiceLabelingSet() ? settings.getChoiceLabelingFilename() : boost::optional<std::string>());
-        // Preprocess the model if needed.
-        model = preprocessModel<ValueType>(model, formulas);
-
-        // Print some information about the model.
-        model->printModelInformationToStream(std::cout);
-
-        // Verify the model, if a formula was given.
-        if (!formulas.empty()) {
-            STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidStateException, "Expected sparse model.");
-            verifySparseModel<ValueType>(model->as<storm::models::sparse::Model<ValueType>>(), formulas);
-        }
-    }
             
         
 }