Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata
Contributor : Hal Ifip Connect in order to contact the contributor
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


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



Irina Măriuca Asăvoae, Frank De Boer, Marcello M. 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


Files downloads