The paper “Sequential Convex Programming for the Efficient Verification of Parametric MDPs” by Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen,
Ivan Papusha, Hasan A. Poonawala, and Ufuk Topcu, and the paper “JANI: Quantitative Model and Tool Interaction” by Carlos E. Budde, Christian Dehnert, Ernst Moritz Hahn, Arnd Hartmanns, Sebastian Junges, and Andrea Turrini have been accepted at TACAS 2017.  JANI consists of an intermediate model language and tool interaction protocol to enable the easy use and comparison of multiple tools for the analysis of probabilistic models. The first paper proposes to use geometric programming for multi-objective verification of parametric Markov decision processes under optimality criteria.