| The goal of this project is to integrate model checking techniques for languages with rich data types, and languages with probabilistic, stochastic, and timing information. The aim is to identify, study and implement model transformations at the language level, in order to minimize state spaces even before their generation, while preserving functional and quantitative properties. Topics of interest are linearization, static analysis, abstraction, and confluence reduction for languages with data and quantitative information. |
