diff --git a/CMakeLists.txt b/CMakeLists.txt
index 9a7bc31be..6c162b7fe 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -169,7 +169,7 @@ find_package(GMP)
 #############################################################
 
 # Boost Option variables
-set(Boost_USE_STATIC_LIBS        ON)
+set(Boost_USE_STATIC_LIBS        ${USE_BOOST_STATIC_LIBRARIES})
 set(Boost_USE_MULTITHREADED      ON)
 set(Boost_USE_STATIC_RUNTIME    OFF)
 
diff --git a/setup.py b/setup.py
index bfa8592c6..a9c58a489 100644
--- a/setup.py
+++ b/setup.py
@@ -51,7 +51,7 @@ class MyEggInfo(egg_info):
 
 class MyInstall(install):
     def run(self):
-        ret = call(["cmake", "-DSTORM_PYTHON=ON",  "-DPYTHON_LIBRARY="+PYTHONLIB, "-DPYTHON_INCLUDE_DIR="+PYTHONINC, os.path.abspath(os.path.dirname(os.path.realpath(__file__)))], cwd=d)
+        ret = call(["cmake", "-DSTORM_PYTHON=ON", "-DUSE_BOOST_STATIC_LIBRARIES=OFF",  "-DPYTHON_LIBRARY="+PYTHONLIB, "-DPYTHON_INCLUDE_DIR="+PYTHONINC, os.path.abspath(os.path.dirname(os.path.realpath(__file__)))], cwd=d)
         if ret != 0:
             raise RuntimeError("Cmake exited with return code {}".format(ret))
         ret = call(["make", "stormpy"], cwd=d)
@@ -60,7 +60,7 @@ class MyInstall(install):
         install.run(self)
 class MyDevelop(develop):
     def run(self):
-       ret = call(["cmake", "-DSTORM_PYTHON=ON",  "-DPYTHON_LIBRARY="+PYTHONLIB, "-DPYTHON_INCLUDE_DIR="+PYTHONINC, os.path.abspath(os.path.dirname(os.path.realpath(__file__)))], cwd=d)
+       ret = call(["cmake", "-DSTORM_PYTHON=ON","-DUSE_BOOST_STATIC_LIBRARIES=OFF",  "-DPYTHON_LIBRARY="+PYTHONLIB, "-DPYTHON_INCLUDE_DIR="+PYTHONINC, os.path.abspath(os.path.dirname(os.path.realpath(__file__)))], cwd=d)
        if ret != 0:
            raise RuntimeError("Cmake exited with return code {}".format(ret))
        ret = call(["make", "stormpy"], cwd=d)
@@ -74,7 +74,10 @@ setup(cmdclass={'install': MyInstall, 'develop': MyDevelop, 'egg_info': MyEggInf
       version="0.2",
       description="Stormpy - Python Bindings for Storm",
       package_dir={'':d},
-      packages=['stormpy', 'stormpy.core', 'stormpy.info'],
-      package_data={'stormpy.core': ['_core.so'], 'stormpy.info' : ['_info.so'] , 'stormpy': ['*.so', '*.dylib', '*.a']},
+      packages=['stormpy', 'stormpy.core', 'stormpy.info', 'stormpy.logic'],
+      package_data={'stormpy.core': ['_core.so'],
+                    'stormpy.logic': ['_logic.so'],
+                    'stormpy.info' : ['_info.so'] ,
+                     'stormpy': ['*.so', '*.dylib', '*.a']},
 
       include_package_data=True)
\ No newline at end of file
diff --git a/src/python/CMakeLists.txt b/src/python/CMakeLists.txt
index 427a3bd30..bc9a1f19e 100644
--- a/src/python/CMakeLists.txt
+++ b/src/python/CMakeLists.txt
@@ -20,27 +20,6 @@ endfunction()
 if(STORM_PYTHON)
     add_python_module(stormpy-info info ${CMAKE_CURRENT_SOURCE_DIR}/storm-info.cpp)
     add_python_module(stormpy-core core ${CMAKE_CURRENT_SOURCE_DIR}/storm-core.cpp)
-
-    #    add_library(stormpy-info SHARED ${CMAKE_CURRENT_SOURCE_DIR}/storm-info.cpp)
-#    target_link_libraries(stormpy-info storm ${BOOST_PYTHON_LIB} ${PYTHON_LIBRARIES})
-#    set_target_properties(stormpy-info PROPERTIES
-#                             OUTPUT_NAME _info
-#                             LIBRARY_OUTPUT_DIRECTORY ${STORMPY_OUTPUT_DIR}/info
-#                             PREFIX ""
-#                             SUFFIX ".so"
-#                            )
-#    add_library(stormpy-core SHARED ${CMAKE_CURRENT_SOURCE_DIR}/storm-core.cpp)
-#    target_link_libraries(stormpy-core storm ${BOOST_PYTHON_LIB} ${PYTHON_LIBRARIES})
-#    set_target_properties(stormpy-core PROPERTIES
-#                             OUTPUT_NAME _core
-#                             LIBRARY_OUTPUT_DIRECTORY ${STORMPY_OUTPUT_DIR}/core
-#                             PREFIX ""
-#                             SUFFIX ".so"
-#                            )
-
-                                                 
-
-    add_custom_target(stormpy DEPENDS stormpy-info stormpy-core)
-
-
+    add_python_module(stormpy-logic logic ${CMAKE_CURRENT_SOURCE_DIR}/storm-logic.cpp)
+    add_custom_target(stormpy DEPENDS stormpy-info stormpy-core stormpy-logic)
 endif()
diff --git a/src/python/storm-core.cpp b/src/python/storm-core.cpp
index 4f9dcd2a5..70d5d719c 100644
--- a/src/python/storm-core.cpp
+++ b/src/python/storm-core.cpp
@@ -30,18 +30,8 @@ BOOST_PYTHON_MODULE(_core)
     using namespace boost::python;
     def("setUp", setupStormLib);
 
-    ////////////////////////////////////////////
-    // Formula
-    ////////////////////////////////////////////
-    class_<storm::logic::Formula, std::shared_ptr<storm::logic::Formula>, boost::noncopyable>("Formula", no_init)
-        .def("__str__", &storm::logic::Formula::toString);
-	class_<std::vector<std::shared_ptr<storm::logic::Formula>>>("FormulaVec")
-			.def(vector_indexing_suite<std::vector<std::shared_ptr<storm::logic::Formula>>, true>())
-			;
-    class_<storm::logic::ProbabilityOperatorFormula, std::shared_ptr<storm::logic::ProbabilityOperatorFormula>, bases<storm::logic::Formula>>("ProbabilityOperatorFormula", no_init)
-        .def("__str__", &storm::logic::ProbabilityOperatorFormula::toString);
 
-    register_ptr_to_python<std::shared_ptr<storm::logic::Formula>>();
+
 
     ////////////////////////////////////////////
     // Program
@@ -92,6 +82,9 @@ BOOST_PYTHON_MODULE(_core)
     defineClass<storm::models::sparse::Dtmc<storm::RationalFunction>,  storm::models::sparse::Model<storm::RationalFunction>>("SparseParametricMc", "");
     defineClass<storm::models::sparse::Mdp<storm::RationalFunction>, storm::models::sparse::Model<storm::RationalFunction>>("SparseParametricMdp", "");
 
+    defineClass<std::vector<std::shared_ptr<storm::logic::Formula>>, void, void>("FormulaVec", "Vector of formulas")
+            .def(vector_indexing_suite<std::vector<std::shared_ptr<storm::logic::Formula>>, true>())
+            ;
 
     def("parse_formulae", storm::parseFormulasForProgram);
     def("parse_program", storm::parseProgram);
diff --git a/src/python/storm-logic.cpp b/src/python/storm-logic.cpp
index e69de29bb..78be3af27 100644
--- a/src/python/storm-logic.cpp
+++ b/src/python/storm-logic.cpp
@@ -0,0 +1,95 @@
+#include <boost/python.hpp>
+#include <boost/python/suite/indexing/vector_indexing_suite.hpp>
+#include "../logic/Formulas.h"
+
+
+#include "helpers.h"
+#include "boostPyExtension.h"
+
+
+
+BOOST_PYTHON_MODULE(_logic)
+{
+    using namespace boost::python;
+
+    ////////////////////////////////////////////
+    // Formula
+    ////////////////////////////////////////////
+    defineClass<storm::logic::Formula, void, boost::noncopyable>("Formula",
+    "Generic Storm Formula")
+        .def("__str__", &storm::logic::Formula::toString)
+    ;
+
+    //
+    // Path Formulae
+    //
+    defineClass<storm::logic::PathFormula, storm::logic::Formula, boost::noncopyable>("PathFormula",
+    "Formula about the probability of a set of paths in an automaton");
+    defineClass<storm::logic::UnaryPathFormula, storm::logic::PathFormula, boost::noncopyable>("UnaryPathFormula",
+    "Path formula with one operand");
+    defineClass<storm::logic::EventuallyFormula, storm::logic::UnaryPathFormula>("EventuallyFormula",
+    "Formula for eventually");
+    defineClass<storm::logic::GloballyFormula, storm::logic::UnaryPathFormula>("GloballyFormula",
+    "Formula for globally");
+    defineClass<storm::logic::BinaryPathFormula, storm::logic::PathFormula, boost::noncopyable>("BinaryPathFormula",
+    "Path formula with two operands");
+    defineClass<storm::logic::BoundedUntilFormula, storm::logic::BinaryPathFormula, boost::noncopyable>("BoundedUntilFormula",
+    "Until Formula with either a step or a time bound.");
+    defineClass<storm::logic::ConditionalPathFormula, storm::logic::BinaryPathFormula>("ConditionalPathFormula",
+    "Path Formula with the right hand side being a condition.");
+    defineClass<storm::logic::UntilFormula, storm::logic::BinaryPathFormula>("UntilFormula",
+    "Path Formula for unbounded until");
+
+
+    //
+    // Reward Path Formulae
+    //
+    defineClass<storm::logic::RewardPathFormula, storm::logic::Formula, boost::noncopyable>("RewardPathFormula",
+    "Formula about the rewards of a set of paths in an automaton");
+    defineClass<storm::logic::CumulativeRewardFormula, storm::logic::RewardPathFormula>("CumulativeRewardFormula",
+    "Summed rewards over a the paths");
+    defineClass<storm::logic::InstantaneousRewardFormula, storm::logic::RewardPathFormula>("InstanteneousRewardFormula",
+    "");
+    defineClass<storm::logic::LongRunAverageRewardFormula, storm::logic::RewardPathFormula>("LongRunAverageRewardFormula",
+    "");
+    defineClass<storm::logic::ReachabilityRewardFormula, storm::logic::RewardPathFormula>("ReachabilityRewardFormula",
+    "");
+
+
+    //
+    // State Formulae
+    //
+    defineClass<storm::logic::StateFormula, storm::logic::Formula, boost::noncopyable>("StateFormula",
+    "Formula about a state of an automaton");
+    defineClass<storm::logic::AtomicExpressionFormula, storm::logic::StateFormula>("AtomicExpressionFormula",
+    "");
+    defineClass<storm::logic::AtomicLabelFormula, storm::logic::StateFormula>("AtomicLabelFormula",
+    "");
+    defineClass<storm::logic::BooleanLiteralFormula, storm::logic::StateFormula>("BooleanLiteralFormula",
+    "");
+    defineClass<storm::logic::UnaryStateFormula, storm::logic::StateFormula, boost::noncopyable>("UnaryStateFormula",
+    "State formula with one operand");
+    defineClass<storm::logic::UnaryBooleanStateFormula, storm::logic::UnaryStateFormula>("UnaryBooleanStateFormula",
+    "");
+    defineClass<storm::logic::OperatorFormula, storm::logic::UnaryStateFormula, boost::noncopyable>("OperatorFormula",
+    "");
+    defineClass<storm::logic::ExpectedTimeOperatorFormula, storm::logic::OperatorFormula>("ExpectedTimeOperator",
+    "The expected time between two events");
+    defineClass<storm::logic::LongRunAverageOperatorFormula, storm::logic::OperatorFormula>("LongRunAvarageOperator",
+    "");
+    defineClass<storm::logic::ProbabilityOperatorFormula, storm::logic::OperatorFormula>("ProbabilityOperator",
+    "");
+    defineClass<storm::logic::RewardOperatorFormula, storm::logic::OperatorFormula>("RewardOperatorFormula",
+    "");
+    defineClass<storm::logic::BinaryStateFormula, storm::logic::StateFormula, boost::noncopyable>("BinaryStateFormula",
+    "State formula with two operands");
+    defineClass<storm::logic::BinaryBooleanStateFormula, storm::logic::BinaryStateFormula>("BooleanBinaryStateFormula",
+    "");
+
+
+
+
+
+
+
+}
\ No newline at end of file
diff --git a/stormpy/logic/__init__.py b/stormpy/logic/__init__.py
index e69de29bb..283bad54d 100644
--- a/stormpy/logic/__init__.py
+++ b/stormpy/logic/__init__.py
@@ -0,0 +1 @@
+from stormpy.logic._logic import *
\ No newline at end of file