Abstracts FLoC 2010

The 2-valued and the 3-Valued Abstraction-Refinement Frameworks in Model Checking

Model checking is a widely used technique for automatic verification of hardware and software systems. Significant amount of research in model checking is devoted to extending its scope to larger and even infinite-state systems. Abstraction is one of the most successful approaches for doing so. It hides some of the irrelevant details of the system, thus resulting in a small (abstract) model whose correct behavior can be checked. Sometimes the abstraction is too coarse and a desired property cannot be checked on the abstract model. In this case, the abstract model is refined by adding some of the hidden details back.

In this talk we present two different frameworks for abstraction-refinement in model checking: The 2-valued (CEGAR) and the 3-valued (TVAR) frameworks. We will describe the abstract models and the type of properties that can be verified with those abstractions. We will also show when refinement is needed. Finally, we will mention some applications of TVAR and try to convince that it is most useful.

Invariant Generation for Probabilistic Programs

Model checking probabilistic programs, typically represented as Markov decision processes, is en vogue. Abstraction-refinement techniques (a la CEGAR) have been developed and parametric model checking approaches have recently been suggested. Prototypical tools support these techniques. Their usage for programs whose invariants are quantitative, i.e., arithmetic expressions in the program variables, is however limited. An alternative is to re- sort to static analysis techniques.

We present a constraint-based method for automatically generating quantitative invariants for probabilistic programs. We show how it can be used, in combination with proof-based methods, to verify properties of probabilistic programs that cannot be analysed by any of currently existing probabilistic model checkers. To our knowledge, this is the first automated method for quantitative- invariant generation.

(Joint work with Larissa Meinicke, Annabelle McIver and Carroll Morgan.)

From validating quantitative models to generating valid ones

Verification techniques for quantitative systems typically require a system model as object of their investigations. Probabilistic model checking is a representative example of this successful approach.

However, emerging needs and constraints of quantitative systems no longer allow for, or benefit from, a complete decoupling of the development of a system from its a posteriori verification.

We paint a somewhat personal picture of what this may mean in terms of challenges and opportunities for those who research the construction of valid quantitative systems.