%0 Conference Proceedings
%T Bounded Model Checking of Recursive Programs with Pointers in K
%+ Alexandru Ioan Cuza University of Iași =  Universitatea Alexandru Ioan Cuza din Iași (UAIC)
%+ Centrum voor Wiskunde en Informatica (CWI)
%+ Leiden Institute of Advanced Computer Science [Leiden] (LIACS)
%A Asăvoae, Irina, Măriuca
%A Boer, Frank, De
%A Bonsangue, Marcello, M.
%A Lucanu, Dorel
%A Rot, Jurriaan
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 21th InternationalWorkshop on Algebraic Development Techniques (WADT)
%C Salamanca, Spain
%Y Narciso Martí-Oliet
%Y Miguel Palomino
%I Springer
%3 Recent Trends in Algebraic Development Techniques
%V LNCS-7841
%P 59-76
%8 2012-06-07
%D 2012
%R 10.1007/978-3-642-37635-1_4
%K pushdown systems
%K model checking
%K the $\mathbb{K}$ framework
%Z Computer Science [cs]Conference papers
%X 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.
%G English
%Z TC 1
%Z WG 1.3
%2 https://inria.hal.science/hal-01485978/document
%2 https://inria.hal.science/hal-01485978/file/978-3-642-37635-1_4_Chapter.pdf
%L hal-01485978
%U https://inria.hal.science/hal-01485978
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-TC1
%~ IFIP-WG1-3
%~ IFIP-LNCS-7841
%~ IFIP-WADT