salle A. Turing CE4
6 décembre 2012 - 15h00
Bounded Model Checking of Recursive Programs with Pointers in K Abstract
par Irina Asavoae de University Alexandru Ioan Cuza, Iasi, Romania
Abstract: We present an adaptation of the model checking pushdown systems to semantics-based verification. First we introduce the algebraic notion of pushdown systems specifications (PSS) and adapt a model checking algorithm for this new notion. Then we instantiate everything in the K framework, namely we show why K is a suitable environment for PSS. Finally, we give a parametric K specification for model checking PSS and show a case study for a PSS that describes recursive programs with pointers for which we model check shape properties of the heap.
