Abstract. Concepts originating from game theory have been employed to formulate and analyse problems from a variety of domains, with applications ranging from economics to biology. In computer science, where they also found a fertile soil, game-theoretic ideas and solutions have been used in AI, network protocols and verification, to name but a few. This thesis sets itself in that context by presenting a framework for verifying concurrent stochastic systems, where agents may compete or cooperate. More specifically, we model systems as concurrent multi-player stochastic games, which are mathematical models able to express environmental uncertainty, nondeterminism and, at each step, the outcomes of the choices made by a set of agents. Given that assuming strict competition among agents does not reflect the full range of system behaviours, we also make use of the notion of social welfare Nash equilibria in order to perform quantitative or qualitative analysis, as well as strategy synthesis, while considering a distinct set of objectives. Equilibria properties and strategies have the advantage of being stable, i.e., they are the result of or a description of rational behaviour, meaning it is actually in the best interest of the agents to act in a way that leads to such an outcome. Verification is also facilitated by the possibility of specifying coalitions, which can translate communication and synchronisation among agents, along with the presentation of a property specification logic for probabilistic and reward-based temporal objectives. Our model checking algorithms for a variant of stopping games make use of linear and nonlinear optimisation along with SMT solvers and are able to verify zero-sum and nonzero-sum properties of concurrent stochastic models. For nonzero-sum properties, our methods focus on computing optimal equilibria, which maximise or minimise the probabilities or rewards associated to a given set of objectives and may include a mixture of finite and infinite-horizon operators. For finite-horizon properties the computation is exact, while for infinite-horizon it is approximate using value iteration. We implement our methods in the PRISM-games 3.0 tool, demonstrating their usefulness and performance on several case studies.