diff --git a/CHANGELOG.md b/CHANGELOG.md
index 726449028..94c0c14b9 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -20,6 +20,8 @@ Version 1.0.x
 - USE_POPCNT removed in favor of FORCE_POPCNT. The popcnt instruction is used if available due to march=native, unless portable is set.
     Then, using FORCE_POPCNT enables the use of the SSE 4.2 instruction
 - Parametric model checking is now handled in a separated library/executable called storm-pars
+- Support for long-run average rewwards on Markov automata using the value-iteration based approach by Butkova et al. (TACAS 17)
+- Support for parsing/building models given in the explicit input format of IMCA.
 
 ### Version 1.0.1 (2017/4)
 
diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp
index eba86792d..bc52f85dc 100644
--- a/src/storm-pars-cli/storm-pars.cpp
+++ b/src/storm-pars-cli/storm-pars.cpp
@@ -155,9 +155,10 @@ namespace storm {
                             regionRefinementCheckResult->writeIllustrationToStream(outStream);
                         }
                     }
+                    outStream << std::endl;
                     STORM_PRINT_AND_LOG(outStream.str());
                 } else {
-                    STORM_PRINT_AND_LOG(*result);
+                    STORM_PRINT_AND_LOG(*result << std::endl);
                 }
                 if (watch) {
                     STORM_PRINT_AND_LOG("Time for model checking: " << *watch << "." << std::endl);
@@ -184,7 +185,9 @@ namespace storm {
             verifyProperties<ValueType>(input.properties,
                                         [&model] (std::shared_ptr<storm::logic::Formula const> const& formula) {
                                             std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::verifyWithSparseEngine<ValueType>(model, storm::api::createTask<ValueType>(formula, true));
-                                            result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
+                                            if (result) {
+                                                result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
+                                            }
                                             return result;
                                         },
                                         [&model] (std::unique_ptr<storm::modelchecker::CheckResult> const& result) {
diff --git a/src/storm/adapters/GmmxxAdapter.h b/src/storm/adapters/GmmxxAdapter.h
index 45f7c5231..dd14ddc4d 100644
--- a/src/storm/adapters/GmmxxAdapter.h
+++ b/src/storm/adapters/GmmxxAdapter.h
@@ -23,7 +23,7 @@ namespace storm {
             template<class T>
             static std::unique_ptr<gmm::csr_matrix<T>> toGmmxxSparseMatrix(storm::storage::SparseMatrix<T> const& matrix) {
                 uint_fast64_t realNonZeros = matrix.getEntryCount();
-                STORM_LOG_DEBUG("Converting matrix with " << realNonZeros << " non-zeros to gmm++ format.");
+                STORM_LOG_DEBUG("Converting " << matrix.getRowCount() << "x" << matrix.getColumnCount() << " matrix with " << realNonZeros << " non-zeros to gmm++ format.");
                 
                 // Prepare the resulting matrix.
                 std::unique_ptr<gmm::csr_matrix<T>> result(new gmm::csr_matrix<T>(matrix.getRowCount(), matrix.getColumnCount()));
diff --git a/src/storm/api/builder.h b/src/storm/api/builder.h
index b2ecc2626..868c47bba 100644
--- a/src/storm/api/builder.h
+++ b/src/storm/api/builder.h
@@ -2,6 +2,7 @@
 
 #include "storm/parser/AutoParser.h"
 #include "storm/parser/DirectEncodingParser.h"
+#include "storm/parser/ImcaMarkovAutomatonParser.h"
 
 #include "storm/storage/SymbolicModelDescription.h"
 
@@ -135,6 +136,16 @@ namespace storm {
         inline std::shared_ptr<storm::models::sparse::Model<storm::RationalNumber>> buildExplicitDRNModel(std::string const&) {
             STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Exact models with direct encoding are not supported.");
         }
+        
+        template<typename ValueType>
+        std::shared_ptr<storm::models::sparse::Model<ValueType>> buildExplicitIMCAModel(std::string const&) {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Exact models with direct encoding are not supported.");
+        }
+        
+        template<>
+        inline std::shared_ptr<storm::models::sparse::Model<double>> buildExplicitIMCAModel(std::string const& imcaFile) {
+            return storm::parser::ImcaMarkovAutomatonParser<double>::parseImcaFile(imcaFile);
+        }
 
 
     }
diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp
index 3284b353c..caf3aa0c3 100644
--- a/src/storm/cli/cli.cpp
+++ b/src/storm/cli/cli.cpp
@@ -380,8 +380,11 @@ namespace storm {
             std::shared_ptr<storm::models::ModelBase> result;
             if (ioSettings.isExplicitSet()) {
                 result = storm::api::buildExplicitModel<ValueType>(ioSettings.getTransitionFilename(), ioSettings.getLabelingFilename(), ioSettings.isStateRewardsSet() ? boost::optional<std::string>(ioSettings.getStateRewardsFilename()) : boost::none, ioSettings.isTransitionRewardsSet() ? boost::optional<std::string>(ioSettings.getTransitionRewardsFilename()) : boost::none, ioSettings.isChoiceLabelingSet() ? boost::optional<std::string>(ioSettings.getChoiceLabelingFilename()) : boost::none);
-            } else {
+            } else if (ioSettings.isExplicitDRNSet()) {
                 result = storm::api::buildExplicitDRNModel<ValueType>(ioSettings.getExplicitDRNFilename());
+            } else {
+                STORM_LOG_THROW(ioSettings.isExplicitIMCASet(), storm::exceptions::InvalidSettingsException, "Unexpected explicit model input type.");
+                result = storm::api::buildExplicitIMCAModel<ValueType>(ioSettings.getExplicitIMCAFilename());
             }
             return result;
         }
@@ -397,7 +400,7 @@ namespace storm {
                 } else if (engine == storm::settings::modules::CoreSettings::Engine::Sparse) {
                     result = buildModelSparse<ValueType>(input, ioSettings);
                 }
-            } else if (ioSettings.isExplicitSet() || ioSettings.isExplicitDRNSet()) {
+            } else if (ioSettings.isExplicitSet() || ioSettings.isExplicitDRNSet() || ioSettings.isExplicitIMCASet()) {
                 STORM_LOG_THROW(engine == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Can only use sparse engine with explicit input.");
                 result = buildModelExplicit<ValueType>(ioSettings);
             }
diff --git a/src/storm/logic/BoundedUntilFormula.cpp b/src/storm/logic/BoundedUntilFormula.cpp
index b954d4720..ff5df2d2a 100644
--- a/src/storm/logic/BoundedUntilFormula.cpp
+++ b/src/storm/logic/BoundedUntilFormula.cpp
@@ -27,6 +27,15 @@ namespace storm {
             return visitor.visit(*this, data);
         }
         
+        void BoundedUntilFormula::gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const {
+            if (this->getTimeBoundReference().isRewardBound()) {
+                referencedRewardModels.insert(this->getTimeBoundReference().getRewardName());
+            }
+            this->getLeftSubformula().gatherReferencedRewardModels(referencedRewardModels);
+            this->getRightSubformula().gatherReferencedRewardModels(referencedRewardModels);
+        }
+        
+        
         TimeBoundReference const& BoundedUntilFormula::getTimeBoundReference() const {
             return timeBoundReference;
         }
@@ -92,7 +101,7 @@ namespace storm {
         template <>
         storm::RationalNumber BoundedUntilFormula::getUpperBound() const {
             checkNoVariablesInBound(this->getUpperBound());
-            storm::RationalNumber bound = this->getLowerBound().evaluateAsRational();
+            storm::RationalNumber bound = this->getUpperBound().evaluateAsRational();
             STORM_LOG_THROW(bound >= storm::utility::zero<storm::RationalNumber>(), storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number.");
             return bound;
         }
@@ -139,6 +148,9 @@ namespace storm {
             this->getLeftSubformula().writeToStream(out);
             
             out << " U";
+            if (this->getTimeBoundReference().isRewardBound()) {
+                out << "{\"" << this->getTimeBoundReference().getRewardName() << "\"}";
+            }
             if (this->hasLowerBound()) {
                 if (this->hasUpperBound()) {
                     if (this->isLowerBoundStrict()) {
diff --git a/src/storm/logic/BoundedUntilFormula.h b/src/storm/logic/BoundedUntilFormula.h
index 754d94cdf..5ff571d84 100644
--- a/src/storm/logic/BoundedUntilFormula.h
+++ b/src/storm/logic/BoundedUntilFormula.h
@@ -20,6 +20,8 @@ namespace storm {
             
             virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
             
+            virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const override;
+            
             TimeBoundReference const& getTimeBoundReference() const;
 
             
diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
index bc83d20f9..722e4c296 100644
--- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
+++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
@@ -284,10 +284,11 @@ namespace storm {
                     }
                     ++numberOfStatesNotInMecs;
                 }
+                uint64_t numberOfSspStates = numberOfStatesNotInMecs + mecDecomposition.size();
                 
                 // Finally, we are ready to create the SSP matrix and right-hand side of the SSP.
                 std::vector<ValueType> b;
-                typename storm::storage::SparseMatrixBuilder<ValueType> sspMatrixBuilder(0, 0, 0, false, true, numberOfStatesNotInMecs + mecDecomposition.size());
+                typename storm::storage::SparseMatrixBuilder<ValueType> sspMatrixBuilder(0, numberOfSspStates , 0, false, true, numberOfSspStates);
                 
                 // If the source state is not contained in any MEC, we copy its choices (and perform the necessary modifications).
                 uint64_t currentChoice = 0;
@@ -328,10 +329,10 @@ namespace storm {
                         boost::container::flat_set<uint64_t> const& choicesInMec = stateChoicesPair.second;
                         
                         for (uint64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) {
-                            std::vector<ValueType> auxiliaryStateToProbabilityMap(mecDecomposition.size());
                             
                             // If the choice is not contained in the MEC itself, we have to add a similar distribution to the auxiliary state.
                             if (choicesInMec.find(choice) == choicesInMec.end()) {
+                                std::vector<ValueType> auxiliaryStateToProbabilityMap(mecDecomposition.size());
                                 b.push_back(storm::utility::zero<ValueType>());
                                 
                                 for (auto element : transitionMatrix.getRow(choice)) {
@@ -363,9 +364,9 @@ namespace storm {
                 }
                 
                 // Finalize the matrix and solve the corresponding system of equations.
-                storm::storage::SparseMatrix<ValueType> sspMatrix = sspMatrixBuilder.build(currentChoice);
+                storm::storage::SparseMatrix<ValueType> sspMatrix = sspMatrixBuilder.build(currentChoice, numberOfSspStates, numberOfSspStates);
                 
-                std::vector<ValueType> x(numberOfStatesNotInMecs + mecDecomposition.size());
+                std::vector<ValueType> x(numberOfSspStates);
                 std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = minMaxLinearEquationSolverFactory.create(sspMatrix);
                 solver->solveEquations(dir, x, b);
                 
diff --git a/src/storm/parser/ImcaMarkovAutomatonParser.cpp b/src/storm/parser/ImcaMarkovAutomatonParser.cpp
new file mode 100644
index 000000000..c00b44497
--- /dev/null
+++ b/src/storm/parser/ImcaMarkovAutomatonParser.cpp
@@ -0,0 +1,276 @@
+#include "storm/parser/ImcaMarkovAutomatonParser.h"
+
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/modules/IOSettings.h"
+#include "storm/settings/modules/CoreSettings.h"
+#include "storm/utility/file.h"
+#include "storm/utility/builder.h"
+
+namespace storm {
+    namespace parser {
+
+        template <typename ValueType, typename StateType>
+        ImcaParserGrammar<ValueType, StateType>::ImcaParserGrammar() : ImcaParserGrammar<ValueType, StateType>::base_type(start), numStates(0), numChoices(0), numTransitions(0), hasStateReward(false), hasActionReward(false) {
+            buildChoiceLabels = storm::settings::getModule<storm::settings::modules::IOSettings>().isBuildChoiceLabelsSet();
+            initialize();
+        }
+        
+        template <typename ValueType, typename StateType>
+        void ImcaParserGrammar<ValueType, StateType>::initialize() {
+            value = qi::double_[qi::_val = qi::_1];
+            value.name("value");
+            
+            // We assume here that imca files are alphanumeric strings, If we restrict ourselves to the 's12345' representation, we could also do:
+            //       state = (qi::lit("s") > qi::ulong_)[qi::_val = qi::_1];
+            state = qi::as_string[qi::raw[qi::lexeme[(qi::alnum | qi::char_('_')) % qi::eps]]][qi::_val = phoenix::bind(&ImcaParserGrammar<ValueType, StateType>::getStateIndex, phoenix::ref(*this), qi::_1)];
+            state.name("state");
+            
+            reward = (-qi::lit("R") >> value)[qi::_val = qi::_1];
+            reward.name("reward");
+            
+            transition = (qi::lit("*") >> state >> value)[qi::_val = phoenix::bind(&ImcaParserGrammar<ValueType, StateType>::createStateValuePair, phoenix::ref(*this), qi::_1, qi::_2)];
+            transition.name("transition");
+            
+            choicelabel = qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')) | qi::lit("!"))]]];
+            choicelabel.name("choicelabel");
+            
+            choice = (state >> choicelabel >> -reward >> *(transition >> qi::eps))[phoenix::bind(&ImcaParserGrammar<ValueType, StateType>::addChoiceToStateBehavior, phoenix::ref(*this), qi::_1, qi::_2, qi::_4, qi::_3)];
+            choice.name("choice");
+            
+            transitions = qi::lit("#TRANSITIONS") >> *(choice);
+            transitions.name("TRANSITIONS");
+            
+            initials = qi::lit("#INITIALS") >> *((state >> qi::eps)[phoenix::bind(&ImcaParserGrammar<ValueType, StateType>::addInitialState, phoenix::ref(*this), qi::_1)]);
+            initials.name("INITIALS");
+            
+            goals = qi::lit("#GOALS") >> *((state >> qi::eps)[phoenix::bind(&ImcaParserGrammar<ValueType, StateType>::addGoalState, phoenix::ref(*this), qi::_1)]);
+            goals.name("GOALS");
+            
+            start = (initials >> goals >> transitions)[qi::_val = phoenix::bind(&ImcaParserGrammar<ValueType, StateType>::createModelComponents, phoenix::ref(*this))];
+            start.name("start");
+
+        }
+        
+        template <typename ValueType, typename StateType>
+        StateType ImcaParserGrammar<ValueType, StateType>::getStateIndex(std::string const& stateString) {
+            auto it = stateIndices.find(stateString);
+            if (it == stateIndices.end()) {
+                this->stateIndices.emplace_hint(it, stateString, numStates);
+                ++numStates;
+                initialStates.grow(numStates);
+                goalStates.grow(numStates);
+                markovianStates.grow(numStates);
+                stateBehaviors.resize(numStates);
+                return numStates - 1;
+            } else {
+                return it->second;
+            }
+        }
+        
+        template <typename ValueType, typename StateType>
+        std::pair<StateType, ValueType> ImcaParserGrammar<ValueType, StateType>::createStateValuePair(StateType const& state, ValueType const& value) {
+            return std::pair<StateType, ValueType>(state, value);
+        }
+        
+        template <typename ValueType, typename StateType>
+        void ImcaParserGrammar<ValueType, StateType>::addInitialState(StateType const& state) {
+            initialStates.set(state);
+        }
+        
+        template <typename ValueType, typename StateType>
+        void ImcaParserGrammar<ValueType, StateType>::addGoalState(StateType const& state) {
+            goalStates.set(state);
+        }
+        
+        template <typename ValueType, typename StateType>
+        void ImcaParserGrammar<ValueType, StateType>::addChoiceToStateBehavior(StateType const& state, std::string const& label, std::vector<std::pair<StateType, ValueType>> const& transitions, boost::optional<ValueType> const& reward) {
+            bool isMarkovian = label == "!";
+            storm::generator::Choice<ValueType, StateType> choice(0, isMarkovian);
+            STORM_LOG_THROW(!transitions.empty(), storm::exceptions::WrongFormatException, "Empty choice defined for state s" << state << ".");
+            if (buildChoiceLabels && !isMarkovian) {
+                choice.addLabel(label);
+            }
+            if (reward && !isMarkovian) {
+                hasActionReward = true;
+                choice.addReward(reward.get());
+            }
+            for (auto const& t : transitions) {
+                STORM_LOG_THROW(t.second > storm::utility::zero<ValueType>(), storm::exceptions::WrongFormatException, "Probabilities and rates have to be positive. got " << t.second << " at state s" << state << ".");
+                choice.addProbability(t.first, t.second);
+            }
+            STORM_LOG_THROW(isMarkovian || storm::utility::isOne(choice.getTotalMass()), storm::exceptions::WrongFormatException, "Probability for choice " << label << " on state s" << state << " does not sum up to one.");
+
+            ++numChoices;
+            numTransitions += choice.size();
+            auto& behavior = stateBehaviors[state];
+            behavior.setExpanded(true);
+            behavior.addChoice(std::move(choice));
+            if (isMarkovian) {
+                markovianStates.set(state);
+                if (reward) {
+                    hasStateReward = true;
+                    behavior.addStateReward(reward.get());
+                }
+            }
+        }
+        
+        template <typename ValueType, typename StateType>
+        storm::storage::sparse::ModelComponents<ValueType> ImcaParserGrammar<ValueType, StateType>::createModelComponents() {
+            
+            // Prepare the statelabeling
+            initialStates.resize(numStates);
+            goalStates.resize(numStates);
+            markovianStates.resize(numStates);
+            storm::models::sparse::StateLabeling stateLabeling(numStates);
+            stateLabeling.addLabel("init", std::move(initialStates));
+            stateLabeling.addLabel("goal", std::move(goalStates));
+            
+            // Fix deadlocks (if required)
+            assert(stateBehaviors.size() == numStates);
+            if (!storm::settings::getModule<storm::settings::modules::CoreSettings>().isDontFixDeadlocksSet()) {
+                StateType state = 0;
+                for (auto& behavior : stateBehaviors) {
+                    if (!behavior.wasExpanded()) {
+                        storm::generator::Choice<ValueType, StateType> choice(0, true);
+                        choice.addProbability(state, storm::utility::one<ValueType>());
+                        behavior.setExpanded(true);
+                        behavior.addChoice(std::move(choice));
+                        markovianStates.set(state);
+                        ++numChoices;
+                        ++numTransitions;
+                    }
+                    ++state;
+                }
+            }
+            
+            // Build the transition matrix together with exit rates, reward models, and choice labeling
+            storm::storage::SparseMatrixBuilder<ValueType> matrixBuilder(numChoices, numStates, numTransitions, true, true, numStates);
+            std::vector<ValueType> exitRates;
+            exitRates.reserve(numStates);
+            boost::optional<std::vector<ValueType>> stateRewards, actionRewards;
+            if (hasStateReward) {
+                stateRewards = std::vector<ValueType>(numStates, storm::utility::zero<ValueType>());
+            }
+            if (hasActionReward) {
+                actionRewards = std::vector<ValueType>(numChoices, storm::utility::zero<ValueType>());
+            }
+            boost::optional<storm::models::sparse::ChoiceLabeling> choiceLabeling;
+            if (buildChoiceLabels) {
+                choiceLabeling = storm::models::sparse::ChoiceLabeling(numChoices);
+            }
+            StateType state = 0;
+            StateType row = 0;
+            for (auto const& behavior : stateBehaviors) {
+                matrixBuilder.newRowGroup(row);
+                if (!behavior.getStateRewards().empty()) {
+                    assert(behavior.getStateRewards().size() == 1);
+                    stateRewards.get()[state] = behavior.getStateRewards().front();
+                }
+                if (markovianStates.get(state)) {
+                    //For Markovian states, the Markovian choice has to be the first one in the resulting transition matrix.
+                    bool markovianChoiceFound = false;
+                    for (auto const& choice : behavior) {
+                        if (choice.isMarkovian()) {
+                            STORM_LOG_THROW(!markovianChoiceFound, storm::exceptions::WrongFormatException, "Multiple Markovian choices defined for state " << state << ".");
+                            markovianChoiceFound = true;
+                            if (!choice.getRewards().empty()) {
+                                assert(choice.getRewards().size() == 1);
+                                actionRewards.get()[row] = choice.getRewards().front();
+                            }
+                            if (buildChoiceLabels && choice.hasLabels()) {
+                                assert(choice.getLabels().size() == 1);
+                                std::string const& label = *choice.getLabels().begin();
+                                if (!choiceLabeling->containsLabel(label)) {
+                                    choiceLabeling->addLabel(label);
+                                }
+                                choiceLabeling->addLabelToChoice(label, row);
+                            }
+                            exitRates.push_back(choice.getTotalMass());
+                            for (auto const& transition : choice) {
+                                matrixBuilder.addNextValue(row, transition.first, static_cast<ValueType>(transition.second / exitRates.back()));
+                            }
+                            ++row;
+                        }
+                    }
+                } else {
+                    exitRates.push_back(storm::utility::zero<ValueType>());
+                }
+                // Now add all probabilistic choices.
+                for (auto const& choice : behavior) {
+                    if (!choice.isMarkovian()) {
+                        if (!choice.getRewards().empty()) {
+                            assert(choice.getRewards().size() == 1);
+                            actionRewards.get()[row] = choice.getRewards().front();
+                        }
+                        if (buildChoiceLabels && choice.hasLabels()) {
+                            assert(choice.getLabels().size() == 1);
+                            std::string const& label = *choice.getLabels().begin();
+                            if (!choiceLabeling->containsLabel(label)) {
+                                choiceLabeling->addLabel(label);
+                            }
+                            choiceLabeling->addLabelToChoice(label, row);
+                        }
+                        for (auto const& transition : choice) {
+                            matrixBuilder.addNextValue(row, transition.first, transition.second);
+                        }
+                        ++row;
+                    }
+                }
+                ++state;
+            }
+            
+            // Finalize the model components
+            std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ValueType>> rewardModel;
+            if (hasStateReward || hasActionReward) {
+                rewardModel.insert(std::make_pair("", storm::models::sparse::StandardRewardModel<ValueType>(stateRewards, actionRewards)));
+            }
+            storm::storage::sparse::ModelComponents<ValueType> components(matrixBuilder.build(), std::move(stateLabeling), std::move(rewardModel), false, std::move(markovianStates));
+            components.exitRates = std::move(exitRates);
+            components.choiceLabeling = std::move(choiceLabeling);
+            
+            return components;
+        }
+
+        template<typename ValueType>
+        std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ImcaMarkovAutomatonParser<ValueType>::parseImcaFile(std::string const& filename) {
+            // Open file and initialize result.
+            std::ifstream inputFileStream;
+            storm::utility::openFile(filename, inputFileStream);
+        
+            storm::storage::sparse::ModelComponents<ValueType> components;
+        
+            // Now try to parse the contents of the file.
+            std::string fileContent((std::istreambuf_iterator<char>(inputFileStream)), (std::istreambuf_iterator<char>()));
+            PositionIteratorType first(fileContent.begin());
+            PositionIteratorType iter = first;
+            PositionIteratorType last(fileContent.end());
+
+            try {
+                // Start parsing.
+                ImcaParserGrammar<ValueType> grammar;
+                bool succeeded = qi::phrase_parse(iter, last, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)) >> (qi::eol | qi::eoi), components);
+                STORM_LOG_THROW(succeeded, storm::exceptions::WrongFormatException, "Could not parse imca file.");
+                STORM_LOG_DEBUG("Parsed imca file successfully.");
+            } catch (qi::expectation_failure<PositionIteratorType> const& e) {
+                STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, e.what_);
+                storm::utility::closeFile(inputFileStream);
+            } catch(std::exception& e) {
+                // In case of an exception properly close the file before passing exception.
+                storm::utility::closeFile(inputFileStream);
+                throw e;
+            }
+            
+            // Close the stream in case everything went smoothly
+            storm::utility::closeFile(inputFileStream);
+            
+            // Build the model from the obtained model components
+            return storm::utility::builder::buildModelFromComponents(storm::models::ModelType::MarkovAutomaton, std::move(components))->template as<storm::models::sparse::MarkovAutomaton<ValueType>>();
+        }
+
+  
+
+        template class ImcaParserGrammar<double>;
+        template class ImcaMarkovAutomatonParser<double>;
+    } // namespace parser
+} // namespace storm
+
diff --git a/src/storm/parser/ImcaMarkovAutomatonParser.h b/src/storm/parser/ImcaMarkovAutomatonParser.h
new file mode 100644
index 000000000..f2820242e
--- /dev/null
+++ b/src/storm/parser/ImcaMarkovAutomatonParser.h
@@ -0,0 +1,76 @@
+#pragma once
+
+#include <memory>
+#include <fstream>
+
+#include "storm/storage/sparse/ModelComponents.h"
+#include "storm/models/sparse/MarkovAutomaton.h"
+#include "storm/generator/StateBehavior.h"
+
+#include "storm/parser/SpiritErrorHandler.h"
+
+namespace storm {
+    namespace parser {
+
+        template <typename ValueType, typename StateType = uint32_t>
+        class ImcaParserGrammar : public qi::grammar<Iterator, storm::storage::sparse::ModelComponents<ValueType>(), Skipper> {
+        
+        public:
+            ImcaParserGrammar();
+            
+        private:
+            void initialize();
+            
+            std::pair<StateType, ValueType> createStateValuePair(StateType const& state, ValueType const& value);
+            StateType getStateIndex(std::string const& stateString);
+            void addInitialState(StateType const& state);
+            void addGoalState(StateType const& state);
+            void addChoiceToStateBehavior(StateType const& state, std::string const& label, std::vector<std::pair<StateType, ValueType>> const& transitions, boost::optional<ValueType> const& reward);
+            storm::storage::sparse::ModelComponents<ValueType> createModelComponents();
+            
+
+            qi::rule<Iterator, storm::storage::sparse::ModelComponents<ValueType>(), Skipper> start;
+            
+            qi::rule<Iterator, qi::unused_type(), Skipper> initials;
+            qi::rule<Iterator, qi::unused_type(), Skipper> goals;
+            qi::rule<Iterator, qi::unused_type(), Skipper> transitions;
+            
+            qi::rule<Iterator, qi::unused_type(), Skipper> choice;
+            qi::rule<Iterator, std::pair<StateType, ValueType>(), Skipper> transition;
+            qi::rule<Iterator, std::string(), Skipper> choicelabel;
+            qi::rule<Iterator, ValueType(), Skipper> reward;
+            qi::rule<Iterator, StateType(), Skipper> state;
+            qi::rule<Iterator, ValueType(), Skipper> value;
+            
+            bool buildChoiceLabels;
+            
+            StateType numStates;
+            StateType numChoices;
+            StateType numTransitions;
+            bool hasStateReward;
+            bool hasActionReward;
+            
+            std::vector<storm::generator::StateBehavior<ValueType, StateType>> stateBehaviors;
+            storm::storage::BitVector initialStates, goalStates, markovianStates;
+            std::map<std::string, StateType> stateIndices;
+
+        };
+
+        template <typename ValueType = double>
+        class ImcaMarkovAutomatonParser {
+        public:
+
+            /*!
+             * Parses the given file under the assumption that it contains a Markov automaton specified in the imca format.
+             *
+             * @param filename The name of the file to parse.
+             * @return The obtained Markov automaton
+             */
+            static std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> parseImcaFile(std::string const& filename);
+
+        };
+  
+
+    } // namespace parser
+} // namespace storm
+
diff --git a/src/storm/settings/modules/IOSettings.cpp b/src/storm/settings/modules/IOSettings.cpp
index 51d7fe512..677b78513 100644
--- a/src/storm/settings/modules/IOSettings.cpp
+++ b/src/storm/settings/modules/IOSettings.cpp
@@ -24,6 +24,8 @@ namespace storm {
             const std::string IOSettings::explicitOptionShortName = "exp";
             const std::string IOSettings::explicitDrnOptionName = "explicit-drn";
             const std::string IOSettings::explicitDrnOptionShortName = "drn";
+            const std::string IOSettings::explicitImcaOptionName = "explicit-imca";
+            const std::string IOSettings::explicitImcaOptionShortName = "imca";
             const std::string IOSettings::prismInputOptionName = "prism";
             const std::string IOSettings::janiInputOptionName = "jani";
             const std::string IOSettings::prismToJaniOptionName = "prism2jani";
@@ -62,6 +64,9 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, explicitDrnOptionName, false, "Parses the model given in the DRN format.").setShortName(explicitDrnOptionShortName)
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("drn filename", "The name of the DRN file containing the model.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build())
                                 .build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, explicitImcaOptionName, false, "Parses the model given in the IMCA format.").setShortName(explicitImcaOptionShortName)
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("imca filename", "The name of the imca file containing the model.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build())
+                                .build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, prismInputOptionName, false, "Parses the model given in the PRISM format.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the PRISM input.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, janiInputOptionName, false, "Parses the model given in the JANI format.")
@@ -136,6 +141,14 @@ namespace storm {
                 return this->getOption(explicitDrnOptionName).getArgumentByName("drn filename").getValueAsString();
             }
 
+            bool IOSettings::isExplicitIMCASet() const {
+                return this->getOption(explicitImcaOptionName).getHasOptionBeenSet();
+            }
+
+            std::string IOSettings::getExplicitIMCAFilename() const {
+                return this->getOption(explicitImcaOptionName).getArgumentByName("imca filename").getValueAsString();
+            }
+
             bool IOSettings::isPrismInputSet() const {
                 return this->getOption(prismInputOptionName).getHasOptionBeenSet();
             }
diff --git a/src/storm/settings/modules/IOSettings.h b/src/storm/settings/modules/IOSettings.h
index d7674e9f2..55f777334 100644
--- a/src/storm/settings/modules/IOSettings.h
+++ b/src/storm/settings/modules/IOSettings.h
@@ -99,6 +99,20 @@ namespace storm {
                  * @return The name of the DRN file that contains the model.
                  */
                 std::string getExplicitDRNFilename() const;
+                
+                /*!
+                 * Retrieves whether the explicit option with IMCA was set.
+                 *
+                 * @return True if the explicit option with IMCA was set.
+                 */
+                bool isExplicitIMCASet() const;
+
+                /*!
+                 * Retrieves the name of the file that contains the model in the IMCA format.
+                 *
+                 * @return The name of the IMCA file that contains the model.
+                 */
+                std::string getExplicitIMCAFilename() const;
 
                 /*!
                  * Retrieves whether the PRISM language option was set.
@@ -312,6 +326,8 @@ namespace storm {
                 static const std::string explicitOptionShortName;
                 static const std::string explicitDrnOptionName;
                 static const std::string explicitDrnOptionShortName;
+                static const std::string explicitImcaOptionName;
+                static const std::string explicitImcaOptionShortName;
                 static const std::string prismInputOptionName;
                 static const std::string janiInputOptionName;
                 static const std::string prismToJaniOptionName;
diff --git a/src/storm/solver/SmtSolver.cpp b/src/storm/solver/SmtSolver.cpp
index 16c16a104..6e66f70f4 100644
--- a/src/storm/solver/SmtSolver.cpp
+++ b/src/storm/solver/SmtSolver.cpp
@@ -91,6 +91,11 @@ namespace storm {
         bool SmtSolver::unsetTimeout() {
             return false;
         }
+        
+        std::string SmtSolver::getSmtLibString() const {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This solver does not support exporting the assertions in the SMT-LIB format.");
+            return "ERROR";
+        }
 
     } // namespace solver
 } // namespace storm
diff --git a/src/storm/solver/SmtSolver.h b/src/storm/solver/SmtSolver.h
index f9184bbd2..3e3a4eeb5 100644
--- a/src/storm/solver/SmtSolver.h
+++ b/src/storm/solver/SmtSolver.h
@@ -71,15 +71,10 @@ namespace storm {
             
 			SmtSolver(SmtSolver const& other) = default;
 
-#ifndef WINDOWS
 			SmtSolver(SmtSolver&& other) = default;
-#endif
 			SmtSolver& operator=(SmtSolver const& other) = default;
-
-#ifndef WINDOWS
 			SmtSolver& operator=(SmtSolver&& other) = default;
-#endif
-            
+   
 			/*!
              * Pushes a backtracking point on the solver's stack. A following call to pop() deletes exactly those
              * assertions from the solver's stack that were added after this call.
@@ -153,10 +148,8 @@ namespace storm {
              * @return Sat if the conjunction of the asserted expressions together with the provided assumptions is
              * satisfiable, Unsat if it is unsatisfiable and Unknown if the solver could not determine satisfiability.
 			 */
-#ifndef WINDOWS
 			virtual CheckResult checkWithAssumptions(std::initializer_list<storm::expressions::Expression> const& assumptions) = 0;
-#endif
-            
+   
 			/*!
              * If the last call to check() or checkWithAssumptions() returned Sat, this method retrieves a model that
              * satisfies all assertions on the solver's stack (as well as provided assumptions), provided that the
@@ -292,6 +285,13 @@ namespace storm {
              */
             virtual bool unsetTimeout();
             
+			/*!
+			 * If supported by the solver, this function returns the current assertions in the SMT-LIB format.
+			 *
+			 * @return the current assertions in the SMT-LIB format.
+			 */
+			virtual std::string getSmtLibString() const;
+			
         private:
             // The manager responsible for the expressions that interact with this solver.
             storm::expressions::ExpressionManager& manager;
diff --git a/src/storm/solver/Z3SmtSolver.cpp b/src/storm/solver/Z3SmtSolver.cpp
index cff81e5e7..13579a172 100644
--- a/src/storm/solver/Z3SmtSolver.cpp
+++ b/src/storm/solver/Z3SmtSolver.cpp
@@ -360,6 +360,15 @@ namespace storm {
             STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
 #endif
         }
+		
+		std::string Z3SmtSolver::getSmtLibString() const {
+#ifdef STORM_HAVE_Z3
+			return solver->to_smt2();
+#else
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
+#endif
+		}
+
 
 	}
 }
diff --git a/src/storm/solver/Z3SmtSolver.h b/src/storm/solver/Z3SmtSolver.h
index ae0981682..6616e0292 100644
--- a/src/storm/solver/Z3SmtSolver.h
+++ b/src/storm/solver/Z3SmtSolver.h
@@ -70,6 +70,8 @@ namespace storm {
             virtual bool setTimeout(uint_fast64_t milliseconds) override;
             
             virtual bool unsetTimeout() override;
+			
+			virtual std::string getSmtLibString() const override;
             
 		private:
 #ifdef STORM_HAVE_Z3