diff --git a/src/formula/abstract/And.h b/src/formula/abstract/And.h
index 3442d62a9..34d4109e2 100644
--- a/src/formula/abstract/And.h
+++ b/src/formula/abstract/And.h
@@ -12,6 +12,7 @@
 #include "src/formula/AbstractFormulaChecker.h"
 #include "src/modelchecker/ForwardDeclarations.h"
 #include <string>
+#include <type_traits>
 
 namespace storm {
 namespace property {
@@ -38,6 +39,10 @@ namespace abstract {
 template <class T, class FormulaType>
 class And : public virtual AbstractFormula<T> {
 
+	// Throw a compiler error when FormulaType is not a subclass of AbstractFormula.
+	static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
+				  "Instantiaton of FormulaType for storm::property::abstract::And<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
+
 public:
 	/*!
 	 * Empty constructor.
diff --git a/src/formula/abstract/BoundedEventually.h b/src/formula/abstract/BoundedEventually.h
index 420dbfff4..25a710b5b 100644
--- a/src/formula/abstract/BoundedEventually.h
+++ b/src/formula/abstract/BoundedEventually.h
@@ -41,6 +41,10 @@ namespace abstract {
 template <class T, class FormulaType>
 class BoundedEventually : public virtual AbstractFormula<T> {
 
+	// Throw a compiler error when FormulaType is not a subclass of AbstractFormula.
+	static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
+				  "Instantiaton of FormulaType for storm::property::abstract::BoundedEventually<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
+
 public:
 	/*!
 	 * Empty constructor
diff --git a/src/formula/abstract/BoundedNaryUntil.h b/src/formula/abstract/BoundedNaryUntil.h
index ccfe2ab17..04d4cc53e 100644
--- a/src/formula/abstract/BoundedNaryUntil.h
+++ b/src/formula/abstract/BoundedNaryUntil.h
@@ -45,6 +45,10 @@ namespace abstract {
 template <class T, class FormulaType>
 class BoundedNaryUntil : public virtual AbstractFormula<T> {
 
+	// Throw a compiler error when FormulaType is not a subclass of AbstractFormula.
+	static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
+				  "Instantiaton of FormulaType for storm::property::abstract::BoundedNaryUntil<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
+
 public:
 	/*!
 	 * Empty constructor
diff --git a/src/formula/abstract/BoundedUntil.h b/src/formula/abstract/BoundedUntil.h
index 33cc4f87a..d7ba66a37 100644
--- a/src/formula/abstract/BoundedUntil.h
+++ b/src/formula/abstract/BoundedUntil.h
@@ -39,6 +39,10 @@ namespace abstract {
 template <class T, class FormulaType>
 class BoundedUntil : public virtual AbstractFormula<T> {
 
+	// Throw a compiler error when FormulaType is not a subclass of AbstractFormula.
+	static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
+				  "Instantiaton of FormulaType for storm::property::abstract::BoundedUntil<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
+
 public:
 	/*!
 	 * Empty constructor
diff --git a/src/formula/abstract/Eventually.h b/src/formula/abstract/Eventually.h
index aa706c311..54754df52 100644
--- a/src/formula/abstract/Eventually.h
+++ b/src/formula/abstract/Eventually.h
@@ -38,6 +38,10 @@ namespace abstract {
 template <class T, class FormulaType>
 class Eventually : public virtual AbstractFormula<T> {
 
+	// Throw a compiler error when FormulaType is not a subclass of AbstractFormula.
+	static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
+				  "Instantiaton of FormulaType for storm::property::abstract::Eventually<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
+
 public:
 	/*!
 	 * Empty constructor
diff --git a/src/formula/abstract/Globally.h b/src/formula/abstract/Globally.h
index 4e0ab0f22..6d3ddb4aa 100644
--- a/src/formula/abstract/Globally.h
+++ b/src/formula/abstract/Globally.h
@@ -39,6 +39,10 @@ namespace abstract {
 template <class T, class FormulaType>
 class Globally : public virtual AbstractFormula<T> {
 
+	// Throw a compiler error when FormulaType is not a subclass of AbstractFormula.
+	static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
+				  "Instantiaton of FormulaType for storm::property::abstract::Globally<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
+
 public:
 	/*!
 	 * Empty constructor
diff --git a/src/formula/abstract/Next.h b/src/formula/abstract/Next.h
index 0688e518b..bf049ad1b 100644
--- a/src/formula/abstract/Next.h
+++ b/src/formula/abstract/Next.h
@@ -38,6 +38,10 @@ namespace abstract {
 template <class T, class FormulaType>
 class Next : public virtual AbstractFormula<T> {
 
+	// Throw a compiler error when FormulaType is not a subclass of AbstractFormula.
+	static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
+				  "Instantiaton of FormulaType for storm::property::abstract::Next<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
+
 public:
 	/*!
 	 * Empty constructor
diff --git a/src/formula/abstract/Not.h b/src/formula/abstract/Not.h
index 6c92e7672..473ca7c64 100644
--- a/src/formula/abstract/Not.h
+++ b/src/formula/abstract/Not.h
@@ -36,6 +36,10 @@ namespace abstract {
 template <class T, class FormulaType>
 class Not : public virtual AbstractFormula<T> {
 
+	// Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
+	static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
+				  "Instantiaton of FormulaType for storm::property::abstract::Not<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
+
 public:
 	/*!
 	 * Empty constructor
diff --git a/src/formula/abstract/Or.h b/src/formula/abstract/Or.h
index 569939c2c..071173c4a 100644
--- a/src/formula/abstract/Or.h
+++ b/src/formula/abstract/Or.h
@@ -36,6 +36,10 @@ namespace abstract {
 template <class T, class FormulaType>
 class Or : public virtual AbstractFormula<T> {
 
+	// Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
+	static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
+				  "Instantiaton of FormulaType for storm::property::abstract::Or<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
+
 public:
 	/*!
 	 * Empty constructor.
diff --git a/src/formula/abstract/PathBoundOperator.h b/src/formula/abstract/PathBoundOperator.h
index 03454b3c5..39f038e30 100644
--- a/src/formula/abstract/PathBoundOperator.h
+++ b/src/formula/abstract/PathBoundOperator.h
@@ -48,6 +48,10 @@ namespace abstract {
 template<class T, class FormulaType>
 class PathBoundOperator : public virtual AbstractFormula<T>, public OptimizingOperator {
 
+	// Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
+	static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
+				  "Instantiaton of FormulaType for storm::property::abstract::PathBoundOperator<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
+
 public:
 	/*!
 	 * Constructor for non-optimizing operator.
diff --git a/src/formula/abstract/PathNoBoundOperator.h b/src/formula/abstract/PathNoBoundOperator.h
index 827b6cfa1..509c12cf3 100644
--- a/src/formula/abstract/PathNoBoundOperator.h
+++ b/src/formula/abstract/PathNoBoundOperator.h
@@ -51,6 +51,12 @@ namespace abstract {
  */
 template <class T, class FormulaType>
 class PathNoBoundOperator: public virtual AbstractFormula<T>, public OptimizingOperator {
+
+	// Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
+	static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
+				  "Instantiaton of FormulaType for storm::property::abstract::PathNoBoundOperator<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
+
+
 public:
 	/*!
 	 * Empty constructor
diff --git a/src/formula/abstract/ProbabilisticBoundOperator.h b/src/formula/abstract/ProbabilisticBoundOperator.h
index d940dccc2..d9b14b183 100644
--- a/src/formula/abstract/ProbabilisticBoundOperator.h
+++ b/src/formula/abstract/ProbabilisticBoundOperator.h
@@ -44,6 +44,10 @@ namespace abstract {
 template<class T, class FormulaType>
 class ProbabilisticBoundOperator : public PathBoundOperator<T, FormulaType> {
 
+	// Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
+	static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
+				  "Instantiaton of FormulaType for storm::property::abstract::ProbabilisticBoundOperator<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
+
 public:
 	/*!
 	 * Empty constructor
diff --git a/src/formula/abstract/ProbabilisticNoBoundOperator.h b/src/formula/abstract/ProbabilisticNoBoundOperator.h
index e1f837ee9..9b276f976 100644
--- a/src/formula/abstract/ProbabilisticNoBoundOperator.h
+++ b/src/formula/abstract/ProbabilisticNoBoundOperator.h
@@ -49,6 +49,11 @@ namespace abstract {
  */
 template <class T, class FormulaType>
 class ProbabilisticNoBoundOperator: public PathNoBoundOperator<T, FormulaType> {
+
+	// Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
+	static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
+				  "Instantiaton of FormulaType for storm::property::abstract::ProbabilisticNoBoundOperator<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
+
 public:
 	/*!
 	 * Empty constructor
diff --git a/src/formula/abstract/RewardBoundOperator.h b/src/formula/abstract/RewardBoundOperator.h
index 5df7be02c..961c11f21 100644
--- a/src/formula/abstract/RewardBoundOperator.h
+++ b/src/formula/abstract/RewardBoundOperator.h
@@ -39,6 +39,10 @@ namespace abstract {
 template<class T, class FormulaType>
 class RewardBoundOperator : public PathBoundOperator<T, FormulaType> {
 
+	// Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
+	static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
+				  "Instantiaton of FormulaType for storm::property::abstract::RewardBoundOperator<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
+
 public:
 	/*!
 	 * Empty constructor
diff --git a/src/formula/abstract/RewardNoBoundOperator.h b/src/formula/abstract/RewardNoBoundOperator.h
index f9dbae5b7..72fb06f6f 100644
--- a/src/formula/abstract/RewardNoBoundOperator.h
+++ b/src/formula/abstract/RewardNoBoundOperator.h
@@ -48,6 +48,11 @@ namespace abstract {
  */
 template <class T, class FormulaType>
 class RewardNoBoundOperator: public PathNoBoundOperator<T, FormulaType> {
+
+	// Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
+	static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
+				  "Instantiaton of FormulaType for storm::property::abstract::RewardNoBoundOperator<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
+
 public:
 	/*!
 	 * Empty constructor
diff --git a/src/formula/abstract/StateBoundOperator.h b/src/formula/abstract/StateBoundOperator.h
index c2f869b9e..56f6b86d9 100644
--- a/src/formula/abstract/StateBoundOperator.h
+++ b/src/formula/abstract/StateBoundOperator.h
@@ -43,6 +43,10 @@ namespace abstract {
 template<class T, class FormulaType>
 class StateBoundOperator : public virtual AbstractFormula<T> {
 
+	// Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
+	static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
+				  "Instantiaton of FormulaType for storm::property::abstract::StateBoundOperator<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
+
 public:
 
 	/*!
diff --git a/src/formula/abstract/StateNoBoundOperator.h b/src/formula/abstract/StateNoBoundOperator.h
index 9696f597d..2fb40145f 100644
--- a/src/formula/abstract/StateNoBoundOperator.h
+++ b/src/formula/abstract/StateNoBoundOperator.h
@@ -49,6 +49,11 @@ namespace abstract {
  */
 template <class T, class FormulaType>
 class StateNoBoundOperator: public virtual AbstractFormula<T> {
+
+	// Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
+	static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
+				  "Instantiaton of FormulaType for storm::property::abstract::StateNoBoundOperator<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
+
 public:
 	/*!
 	 * Empty constructor
diff --git a/src/formula/abstract/SteadyStateBoundOperator.h b/src/formula/abstract/SteadyStateBoundOperator.h
index 2c5d33bd4..3bbb7f88c 100644
--- a/src/formula/abstract/SteadyStateBoundOperator.h
+++ b/src/formula/abstract/SteadyStateBoundOperator.h
@@ -32,6 +32,10 @@ namespace abstract {
 template <class T, class FormulaType>
 class SteadyStateBoundOperator : public StateBoundOperator<T, FormulaType> {
 
+	// Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
+	static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
+				  "Instantiaton of FormulaType for storm::property::abstract::SteadyStateBoundOperator<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
+
 public:
 	/*!
 	 * Empty constructor
diff --git a/src/formula/abstract/SteadyStateNoBoundOperator.h b/src/formula/abstract/SteadyStateNoBoundOperator.h
index 4831c1743..88fe73ead 100644
--- a/src/formula/abstract/SteadyStateNoBoundOperator.h
+++ b/src/formula/abstract/SteadyStateNoBoundOperator.h
@@ -29,6 +29,11 @@ namespace abstract {
  */
 template <class T, class FormulaType>
 class SteadyStateNoBoundOperator: public StateNoBoundOperator<T, FormulaType> {
+
+	// Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
+	static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
+				  "Instantiaton of FormulaType for storm::property::abstract::SteadyStateNoBoundOperator<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
+
 public:
 	/*!
 	 * Empty constructor
diff --git a/src/formula/abstract/TimeBoundedEventually.h b/src/formula/abstract/TimeBoundedEventually.h
index 362692ba4..23d0fd74f 100644
--- a/src/formula/abstract/TimeBoundedEventually.h
+++ b/src/formula/abstract/TimeBoundedEventually.h
@@ -25,6 +25,11 @@ namespace abstract {
  */
 template<class T, class FormulaType>
 class TimeBoundedEventually: public storm::property::abstract::TimeBoundedOperator<T> {
+
+	// Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
+	static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
+				  "Instantiaton of FormulaType for storm::property::abstract::TimeBoundedEventually<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
+
 public:
 	/**
 	 * Simple constructor: Only sets the bounds
diff --git a/src/formula/abstract/TimeBoundedUntil.h b/src/formula/abstract/TimeBoundedUntil.h
index 823ac8fd0..146c82cd1 100644
--- a/src/formula/abstract/TimeBoundedUntil.h
+++ b/src/formula/abstract/TimeBoundedUntil.h
@@ -25,6 +25,11 @@ namespace abstract {
  */
 template <class T, class FormulaType>
 class TimeBoundedUntil: public TimeBoundedOperator<T> {
+
+	// Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
+	static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
+				  "Instantiaton of FormulaType for storm::property::abstract::TimeBoundedUntil<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
+
 public:
 	/**
 	 * Constructor providing bounds only;
diff --git a/src/formula/abstract/Until.h b/src/formula/abstract/Until.h
index 5037ad018..1df330926 100644
--- a/src/formula/abstract/Until.h
+++ b/src/formula/abstract/Until.h
@@ -38,6 +38,10 @@ namespace abstract {
 template <class T, class FormulaType>
 class Until : public virtual AbstractFormula<T> {
 
+	// Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
+	static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
+				  "Instantiaton of FormulaType for storm::property::abstract::Until<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
+
 public:
 	/*!
 	 * Empty constructor