# Bounded Model Checking of Recursive Programs with Pointers in K

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 $\mathbb{K}$ framework by means of Shylock, a relevant PSS example. We show why $\mathbb{K}$ is a suitable environment for the pushdown system specifications and we give a methodology for defining the PSS in $\mathbb{K}$. Finally, we give a parametric $\mathbb{K}$ specification for model checking pushdown system specifications based on the adapted model checking algorithm for PSS.
Keywords :
Document type :
Conference papers
Domain :

https://hal.inria.fr/hal-01485978
Contributor : Hal Ifip <>
Submitted on : Thursday, March 9, 2017 - 3:33:41 PM
Last modification on : Wednesday, December 20, 2017 - 5:42:07 PM
Long-term archiving on: : Saturday, June 10, 2017 - 2:23:27 PM

### File

978-3-642-37635-1_4_Chapter.pd...
Files produced by the author(s)

### Citation

Irina Asăvoae, Frank Boer, Marcello Bonsangue, Dorel Lucanu, Jurriaan Rot. Bounded Model Checking of Recursive Programs with Pointers in K. 21th InternationalWorkshop on Algebraic Development Techniques (WADT), Jun 2012, Salamanca, Spain. pp.59-76, ⟨10.1007/978-3-642-37635-1_4⟩. ⟨hal-01485978⟩

Record views