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. © IFIP International Federation for Information Processing 2013.
Author supplied keywords
Cite
CITATION STYLE
Asǎvoae, I. M., De Boer, F., Bonsangue, M. M., Lucanu, D., & Rot, J. (2013). Bounded model checking of recursive programs with pointers in K. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7841 LNCS, pp. 59–76). https://doi.org/10.1007/978-3-642-37635-1_4
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
