Model Checking is nowadays a mature field of research, being awarded a Turing award in 2007. It consists in describing formally a system in the form of a mathematical model, specifying the properties it has to fulfill in a formal logic, and providing algorithms to decide whether the model satisfies the property. Model checking started with Boolean systems and properties, sequential finite state models, etc. This is now well established. In order to handle realistic (and thus large) systems, abstractions techniques such as the so called CEGAR method, namely counter example guided abstraction refinement (see e.g. [CCKSVW02]), or abstract interpretation (see the work of Cousot et al.) have been developed. These methods work extremely well for verifying (large, sequential) programs, where Boolean predicates (e.g. variable x is below value a) are well suited. However, current abstraction techniques are not suited to the verification of large stochastic systems. To verify large stochastic systems, techniques such as Statistical Model Checking (based on Monte Carlo property testing) can be used. However, the latter do not give sure answers, but only answers correct up to some probabilities. To date, there is no (sure) Model Checking method which scales to large stochastic systems (e.g. Markov Chains with 10^20 states and over, for instance 20 variables which can take 10 different values each). For instance, the PRISM model checker and other comparable tools scale up to 10^10 states. This is the main reason why Clarke, Cousot et al. launched the CMACS initiative (Computational Modeling and Analysis for Complex Systems) in order to create MCAI 2.0, the next-generation Model Checking and Abstract Interpretation. The aim of our research project Stoch-MC is to develop scalable model checking techniques that can handle large stochastic systems and give sure answers. Large stochastic systems arise naturally in many different contexts, from networks to system biology. We will demonstrate the techniques on two key stochastic models: a model for Hela cells death and a model of stress response in yeast. Our key idea to obtain scalable algorithms is that probabilities can be approximated. A bound on the error made by the approximation is computed a posteriori, based on the characteristics of the model. We thus obtain a probability range (e.g. [0.4, 0.6]) instead of a precise point value as in current model checkers. If the answer is not precise enough (e.g. we want to know whether the probability is bigger than 0.45), then more time is devoted to the approximation, such that the error decreases, until a definite answer can be given. This mimics the CEGAR method in spirit. The method thus calls for several tools. First, parametric algorithms should be proposed which can perform good approximated analysis. The parameter allows making it more precise at the expense of computational time. Second, an error analysis should be proposed, in order to evaluate a bound on the error. Some preliminary approaches have already been proposed by us, see [AAGT12, PALGT12]. Ultimately, we want to model check large Markov Decision Processes (MDPs). In the realm of system biology, compared to Markov Chains, MDPs allows model with different modes (e.g. pathway saturated/non-saturated by a drug). Also, MDPs allow to model different possibilities (the amount of drug to put at some moment, etc). Model checking a MDP thus amounts to finding optimal choices according to a given reward function, for instance designing cells with the right behavior. We believe that designing scalable model checking techniques for large MDPs against a full version of the logic is not doable in the next 4 years. We will however develop techniques for every key feature and demonstrate them on biological pathways, forming a proof of concept that scalable (sure) model checking that can handle large MDPs is feasible, and will be the basis of an ERC project proposal in 4 years.