Verification

  Programmcode Copyright: Martin Braun

These applications include: randomized distributed algorithms, where randomization breaks the symmetry between processes; security, for example key generation at encryption; systems biology, where species randomly react depending on their concentration; robot programs interacting with unknown and varying environments; and so forth. Whereas initial approaches in the 1980s by Vardi and Hart et al. focused on qualitative properties of finite-state systems, in the last two decades significant algorithmic advances have been achieved so as to formally check properties involving quantities. This has led to probabilistic model-checking techniques to prove properties specified by, for example, probabilistic ω-regular languages or probabilistic temporal logics such as PCTL, as well as deductive techniques using variants of Hoare logic and theorem proving. PRISM, MRMC, and CADP are mature probabilistic model checkers that have been applied successfully to a wide range of benchmarks. Extensions of interactive theorem provers such as Isabelle and HOL with probabilistic reasoning are under development; these could, for example, play a role for the aforementioned dissertation project. Alur and others recently identified probabilistic verification as a promising new direction as it establishes correctness and evaluates performance and dependability aspects in an integrated framework. Current trends in this field include to bridge the gap between automated techniques and probabilistic program analysis, parameter synthesis, considering richer models, such as probabilistic hybrid models and probabilistic tree automata and richer property classes, such as timed automata, conditional probabilities, quantiles, and multi-objective properties.The following subsections describe five sample dissertation projects within the research thrust Verification.