diff --git a/CMakeLists.txt b/CMakeLists.txt
index 46b02df5c..bf0d72079 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -26,6 +26,7 @@ option(LINK_LIBCXXABI "Sets whether libc++abi should be linked." OFF)
 option(USE_LIBCXX "Sets whether the standard library is libc++." OFF)
 option(USE_CARL "Sets whether carl should be included." ON)
 option(FORCE_COLOR "Force color output" OFF)
+option(STOMR_COMPILE_WITH_CCACHE "Compile using CCache" ON)
 set(GUROBI_ROOT "" CACHE STRING "A hint to the root directory of Gurobi (optional).")
 set(Z3_ROOT "" CACHE STRING "A hint to the root directory of Z3 (optional).")
 set(CUDA_ROOT "" CACHE STRING "The root directory of CUDA.")
@@ -43,7 +44,16 @@ endif()
 message(STATUS "StoRM - Building ${CMAKE_BUILD_TYPE} version.")
 message(STATUS "StoRM - CMAKE_BUILD_TYPE (ENV): $ENV{CMAKE_BUILD_TYPE}")
 
-
+if(STOMR_COMPILE_WITH_CCACHE)
+	find_program(CCACHE_FOUND ccache)
+	if(CCACHE_FOUND)
+		message(STATUS "SToRM - Using ccache")
+		set_property(GLOBAL PROPERTY RULE_LAUNCH_COMPILE ccache)
+		set_property(GLOBAL PROPERTY RULE_LAUNCH_LINK ccache)
+	else()
+		message(STATUS "Could not find ccache")
+	endif()
+endif()
 
 # Base path for test files
 set(STORM_CPP_TESTS_BASE_PATH "${PROJECT_SOURCE_DIR}/test")
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/logic/Formula.cpp b/src/logic/Formula.cpp
index 4037cb723..e621c1c78 100644
--- a/src/logic/Formula.cpp
+++ b/src/logic/Formula.cpp
@@ -1,4 +1,5 @@
 #include "src/logic/Formulas.h"
+#include <sstream>
 
 namespace storm {
     namespace logic {
@@ -404,6 +405,12 @@ namespace storm {
             return;
         }
         
+        std::string Formula::toString() const {
+            std::stringstream str2;
+            writeToStream(str2);
+            return str2.str();
+        }
+        
         std::ostream& operator<<(std::ostream& out, Formula const& formula) {
             return formula.writeToStream(out);
         }
diff --git a/src/logic/Formula.h b/src/logic/Formula.h
index 3c3c3b5aa..4d831e456 100644
--- a/src/logic/Formula.h
+++ b/src/logic/Formula.h
@@ -174,6 +174,7 @@ namespace storm {
             std::shared_ptr<Formula const> asSharedPointer();
             std::shared_ptr<Formula const> asSharedPointer() const;
             
+            std::string toString() const;
             virtual std::ostream& writeToStream(std::ostream& out) const = 0;
             
             virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const;
diff --git a/src/utility/storm.h b/src/utility/storm.h
index 7fa547588..19f84b85d 100644
--- a/src/utility/storm.h
+++ b/src/utility/storm.h
@@ -170,28 +170,26 @@ namespace storm {
         STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for parametric model.");
     }
 #endif
-            
+
     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;
-            if (model->getType() == storm::models::ModelType::Dtmc) {
-                std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> dtmc = model->template as<storm::models::sparse::Dtmc<ValueType>>();
-                storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> modelchecker(*dtmc);
-                if (modelchecker.canHandle(*formula)) {
-                    result = modelchecker.check(*formula);
-                } else {
-                    storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<ValueType>> modelchecker2(*dtmc);
-                    if (modelchecker2.canHandle(*formula)) {
-                        result = modelchecker2.check(*formula);
-                    }
+    std::unique_ptr<storm::modelchecker::CheckResult> verifySparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::shared_ptr<storm::logic::Formula> const& formula) {
+
+        std::unique_ptr<storm::modelchecker::CheckResult> result;
+        if (model->getType() == storm::models::ModelType::Dtmc) {
+            std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> dtmc = model->template as<storm::models::sparse::Dtmc<ValueType>>();
+            storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> modelchecker(*dtmc);
+            if (modelchecker.canHandle(*formula)) {
+                result = modelchecker.check(*formula);
+            } else {
+                storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<ValueType>> modelchecker2(*dtmc);
+                if (modelchecker2.canHandle(*formula)) {
+                    result = modelchecker2.check(*formula);
                 }
-            } else if (model->getType() == storm::models::ModelType::Mdp) {
-                std::shared_ptr<storm::models::sparse::Mdp<ValueType>> mdp = model->template as<storm::models::sparse::Mdp<ValueType>>();
+            }
+        } else if (model->getType() == storm::models::ModelType::Mdp) {
+            std::shared_ptr<storm::models::sparse::Mdp<ValueType>> mdp = model->template as<storm::models::sparse::Mdp<ValueType>>();
 #ifdef STORM_HAVE_CUDA
-                if (settings.isCudaSet()) {
+            if (settings.isCudaSet()) {
                     storm::modelchecker::TopologicalValueIterationMdpPrctlModelChecker<ValueType> modelchecker(*mdp);
                     result = modelchecker.check(*formula);
                 } else {
@@ -199,26 +197,19 @@ namespace storm {
                     result = modelchecker.check(*formula);
                 }
 #else
-                storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> modelchecker(*mdp);
-                result = modelchecker.check(*formula);
+            storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> modelchecker(*mdp);
+            result = modelchecker.check(*formula);
 #endif
-            } else if (model->getType() == storm::models::ModelType::Ctmc) {
-                std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> ctmc = model->template as<storm::models::sparse::Ctmc<ValueType>>();
+        } else if (model->getType() == storm::models::ModelType::Ctmc) {
+            std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> ctmc = model->template as<storm::models::sparse::Ctmc<ValueType>>();
 
-                storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<ValueType>> modelchecker(*ctmc);
-                result = modelchecker.check(*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;
-            }
+            storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<ValueType>> modelchecker(*ctmc);
+            result = modelchecker.check(*formula);
         }
+        return result;
+
     }
+
             
 #ifdef STORM_HAVE_CARL
     inline void exportParametricResultToFile(storm::RationalFunction const& result, storm::models::sparse::Dtmc<storm::RationalFunction>::ConstraintCollector const& constraintCollector, std::string const& path) {
@@ -236,163 +227,71 @@ 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) {
+    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>>();
 
-        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>>();
+        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;
+    }
+            
 
-            std::cout << std::endl << "Model checking property: " << *formula << " ...";
-            std::unique_ptr<storm::modelchecker::CheckResult> result;
+#endif
 
-            storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>> modelchecker(*dtmc);
+    template<storm::dd::DdType DdType>
+    std::unique_ptr<storm::modelchecker::CheckResult> verifySymbolicModelWithHybridEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::shared_ptr<storm::logic::Formula> const& formula) {
+        std::unique_ptr<storm::modelchecker::CheckResult> result;
+        if (model->getType() == storm::models::ModelType::Dtmc) {
+            std::shared_ptr<storm::models::symbolic::Dtmc<DdType>> dtmc = model->template as<storm::models::symbolic::Dtmc<DdType>>();
+            storm::modelchecker::HybridDtmcPrctlModelChecker<DdType, double> 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;
+        } else if (model->getType() == storm::models::ModelType::Ctmc) {
+            std::shared_ptr<storm::models::symbolic::Ctmc<DdType>> ctmc = model->template as<storm::models::symbolic::Ctmc<DdType>>();
+            storm::modelchecker::HybridCtmcCslModelChecker<DdType, double> modelchecker(*ctmc);
+            if (modelchecker.canHandle(*formula)) {
+                result = modelchecker.check(*formula);
             }
-
-            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());
+        } else if (model->getType() == storm::models::ModelType::Mdp) {
+            std::shared_ptr<storm::models::symbolic::Mdp<DdType>> mdp = model->template as<storm::models::symbolic::Mdp<DdType>>();
+            storm::modelchecker::HybridMdpPrctlModelChecker<DdType, double> modelchecker(*mdp);
+            if (modelchecker.canHandle(*formula)) {
+                result = modelchecker.check(*formula);
             }
+        } else {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented.");
         }
+        return result;
     }
-#endif
-            
-    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;
-            if (model->getType() == storm::models::ModelType::Dtmc) {
-                std::shared_ptr<storm::models::symbolic::Dtmc<DdType>> dtmc = model->template as<storm::models::symbolic::Dtmc<DdType>>();
-                storm::modelchecker::HybridDtmcPrctlModelChecker<DdType, double> modelchecker(*dtmc);
-                if (modelchecker.canHandle(*formula)) {
-                    result = modelchecker.check(*formula);
-                }
-            } else if (model->getType() == storm::models::ModelType::Ctmc) {
-                std::shared_ptr<storm::models::symbolic::Ctmc<DdType>> ctmc = model->template as<storm::models::symbolic::Ctmc<DdType>>();
-                storm::modelchecker::HybridCtmcCslModelChecker<DdType, double> modelchecker(*ctmc);
-                if (modelchecker.canHandle(*formula)) {
-                    result = modelchecker.check(*formula);
-                }
-            } else if (model->getType() == storm::models::ModelType::Mdp) {
-                std::shared_ptr<storm::models::symbolic::Mdp<DdType>> mdp = model->template as<storm::models::symbolic::Mdp<DdType>>();
-                storm::modelchecker::HybridMdpPrctlModelChecker<DdType, double> modelchecker(*mdp);
-                if (modelchecker.canHandle(*formula)) {
-                    result = modelchecker.check(*formula);
-                }
-            } else {
-                STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented.");
-            }
 
-            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>
-    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;
-            if (model->getType() == storm::models::ModelType::Dtmc) {
-                std::shared_ptr<storm::models::symbolic::Dtmc<DdType>> dtmc = model->template as<storm::models::symbolic::Dtmc<DdType>>();
-                storm::modelchecker::SymbolicDtmcPrctlModelChecker<DdType, double> modelchecker(*dtmc);
-                if (modelchecker.canHandle(*formula)) {
-                    result = modelchecker.check(*formula);
-                }
-            } else if (model->getType() == storm::models::ModelType::Mdp) {
-                std::shared_ptr<storm::models::symbolic::Mdp<DdType>> mdp = model->template as<storm::models::symbolic::Mdp<DdType>>();
-                storm::modelchecker::SymbolicMdpPrctlModelChecker<DdType, double> modelchecker(*mdp);
-                if (modelchecker.canHandle(*formula)) {
-                    result = modelchecker.check(*formula);
-                }
-            } else {
-                STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented.");
-            }
 
-            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) {
+        std::unique_ptr<storm::modelchecker::CheckResult> result;
+        if (model->getType() == storm::models::ModelType::Dtmc) {
+            std::shared_ptr<storm::models::symbolic::Dtmc<DdType>> dtmc = model->template as<storm::models::symbolic::Dtmc<DdType>>();
+            storm::modelchecker::SymbolicDtmcPrctlModelChecker<DdType, double> modelchecker(*dtmc);
+            if (modelchecker.canHandle(*formula)) {
+                result = modelchecker.check(*formula);
             }
-        }
-    }
-            
-     
-    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.");
+        } else if (model->getType() == storm::models::ModelType::Mdp) {
+            std::shared_ptr<storm::models::symbolic::Mdp<DdType>> mdp = model->template as<storm::models::symbolic::Mdp<DdType>>();
+            storm::modelchecker::SymbolicMdpPrctlModelChecker<DdType, double> modelchecker(*mdp);
+            if (modelchecker.canHandle(*formula)) {
+                result = modelchecker.check(*formula);
             }
+        } else {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented.");
         }
-    }
-            
-    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);
-        }
+        return result;
     }