by Flemming Nielson
The second annual meeting of the ERCIM Working Group on Models and Logics for Quantitative Analysis (MLQA) took place on Friday July 9th 2010 as part of the Federated Logic Conference (FLoC) organized by the School of Informatics at the University of Edinburgh in Scotland. It was attended by more than 30 researchers, from senior researchers to PhD students, and was one of the best attended satellite events taking place at FLoC.
The meeting focused on the interplay between static analysis and model checking for verifying and validating IT Systems. Professor Bernhard Steffen, who was perhaps the first researcher to suggest that many static analysis problems can be encoded as model checking problems, gave an overview of how these results emerged two decades ago and the clarity they brought to understanding complex data flow analysis problems and how best to implement them. Professor Steffen’s overview was supplemented by Professor Flemming Nielson, who presented recent results showing that state-of-the-art techniques for static analysis, particularly Computation Tree Logic (CTL), can also be used for model checking. This suggests that static analysis and model checking are more similar than classical wisdom would suggest and that algorithmic techniques should be transferred between fields.
Left: The chairman of MLQA, Professor Flemming Nielson, opens the meeting. Right: MLQA workshop participants.
Abstraction techniques, lying at the core of static analysis, have for many years been used to reduce the state explosion usually incurred in model checking by introducing uncertainty to cut down on the amount of detail incorporated. In his talk on partial models and software model checking, Dr Arie Gurfinkel gave an overview of a symbolic model checker that allows partial models to interact with the Counterexample-Guided Abstraction Refinement (CEGAR) framework that is an effective technique for gradually increasing the size of models in case a property cannot be established or refuted. This was followed by recent results on Three-Valued Abstraction-Refinement (TVAR), by professor Orna Grumberg, where a third truth value is used to represent the uncertainty, covering examples of its use and a study of the kind of properties that can be verified.
The quantitative dimension focused on validating stochastic properties on systems with probabilistic choices possibly also including nondeterminism. A main challenge is how to extend the abstraction techniques, which work so well in the discrete dimension, to be able to deal with probabilities. Professor Marta Kwiatkowska showed how to use ideas from two-player games to achieve this. Analysing programs mixing probabilities and nondeterminism in a parametric way poses serious challenges, discussed in the presentation by Professor Joost-Pieter Katoen, that showed how to generalize Hoare’s axiomatic approach to work with distributions by constructing invariants for linear probabilistic programs.
The challenges of analysing nondeterministic iterative programs were outlined by Dr David Monniaux, whose presentation focused on using techniques other than the abstraction and approximation techniques of Abstract Interpretation, one of the key approaches to static analysis. Instead linear programming techniques and methods from game theory were adapted to construct suitable abstractions. The final presentation, by Dr Michael Huth, “turned the problem upside down” by moving the emphasis from the a posteori validation of IT Systems to a more holistic approach to the construction of systems guaranteed to live up to quantitative expectations.
In a final business meeting a steering committee was formed for planning the upcoming activities of the working group and for creating links with other communities of researchers sharing in part the vision of MLQA, in particular the community on Quantitative Aspects of Programming Languages (QAPL). The steering committee is comprised of Flemming Nielson (Technical University of Denmark), Diego Latella (ISTI-CNR in Pisa), Joost-Pieter Katoen (RWTH Aachen), Herbert Wiklicky (Imperial College London), Erik de Vink (Eindhoven University of Technology) and Catuscia Palamidessi (INRIA and Ecole Polytechnique).
For more information please consult the MLQA wiki where most of the presentations are available and where details of the next meeting in 2011 will be posted as well as the plans for further stimulating interaction among members of the working group.
Link: http://wiki.ercim.eu/wg/MLQA/
Please contact:
Flemming Nielson
ERCIM MLQA Working Group coordinator
DTU (Technical University of Denmark) Informatics, Denmark
E-mail:
