| Year | 2012 |
|---|---|
| Type | Conference |
| Status | Proceedings |
| Authors | Irina Asavoae, Frank de Boer, Marcello Bonsangue, Dorel Lucanu, Jurriann Rot |
Links
Abstract
We present an adaptation of model-based verification, via model checking pushdown systems, to semantics-based verification. First we introduce the algebraic notion of pushdown system specifications (PSS) and adapt a model checking algorithm for this new notion. We instantiate pushdown system specifications in the \K framework by means of Shylock, a relevant PSS example. We show why \K is a suitable environment for the pushdown system specifications and we give a methodology for defining the PSS in \K. Finally, we give a parametric \K specification for model checking pushdown system specifications based on the adapted model checking algorithm for PSS.
BibTeX
@Proceedings{name,
author = {Irina~Mariuca~Asavoae and Frank~de~Boer and Marcello~Bonsangue and Dorel~Lucanu and Jurriaan~Rot},
title = {Bounded Model Checking of Recursive Programs with Pointers in K},
booktitle = {WADT 2012},
series = {LNCS},
pages = {},
year = {2012},
volume = {},
number = {},
publisher = {},
url_publisher = {},
note = {to appaer},
url = {http://maude.sip.ucm.es/wadt2012/[WADT2012]}
}