Invited speakers (confirmed)
 |
 |
| Parosh Abdulla | Marta Kwiatkowska |
| Uppsala University, Sweden | Trinity College, Oxford, UK |
Parosh Abdulla
Cut-offs in Parameterized Verification
The "parameterized verification problem" is to prove or refute that some specification is true for all values of the parameters. The parameters may relate to the size or topology of a network, to data types over which a system is constructed, to initial values of variables, etc.
There is strong empirical evidence that many classes of parameterized systems often enjoy a small model property, in the sense that analyzing only a small number of processes (rather than the whole family) is sufficient to capture the reachability of bad configurations.
We introduce a method that exploits the small model property, and performs parameterized verification by only inspecting a small set of fixed instances of the system. The method relies on an abstraction function that views the system from the perspective of a fixed number of processes. The abstraction is used during the verification procedure in order to dynamically detect cut-off points beyond which the search of the state space need not continue.
Our experimentation on a variety of benchmarks demonstrate that the method is highly efficient and that it works well even for classes of systems with undecidable verification problems. Such systems include mutual exclusion protocols, cache coherence protocols, concurrent data structures, and programs operating on unbounded structures such as stacks and queues.
Marta Kwiatkowska
Parameter synthesis for probabilistic real-time systems
The parameter synthesis problem aims to find parameter valuations that guarantee that a given objective is satisfied for a parametric model. Applications range from automated model repair to optimisation. This lecture will focus on models with probability and real-time and give an overview of recent results concerning parameter synthesis from quantitative temporal logic objectives. Existing algorithmic approaches and experimental results will be discussed, and future research challenges outlined.