Abstracts FLoC 2010

Joost-Pieter Katoen. 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.)

Orna Grumberg. 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.

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.

Policy iteration for static analysis

Static analysis by abstract interpretation has traditionally computed over-approximations of least fixed points (loops or recursive functions) using Kleene iteration accelerated by widening operators. In recent years, techniques inspired from game theory have been applied to fixpoint problems in certain abstract domains: min-policy iterations (E. Goubault's group) and max-policy iterations (H. Seidl's group). We shall outline these techniques.

Finally, we shall discuss recent results, obtained with T. Gawlitza, about the computation of least fixed points from succinct representations of programs, giving the same precision as explicitly distinguishing all program paths but with the same exponential complexity as the coarse analysis that merges program paths (a naive approach would incur double exponential complexity). The succinct representation is exploited through SMT-solving.

We would appreciate insights for possible applications of such techniques to succinct representations of e.g. probabilistic systems.