Verimag

Seminar details

salle A. Turing CE4
6 December 2012 - 15h00
Bounded Model Checking of Recursive Programs with Pointers in K Abstract
by Irina Asavoae from 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.





Contact | Site Map | Site powered by SPIP 3.0.26 + AHUNTSIC [CC License]

info visites 916505