Bounded Model Checking of Recursive Programs with Pointers in K - Recent Trends in Algebraic DevelopmentTechniques
Conference Papers Year : 2013

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.
Fichier principal
Vignette du fichier
978-3-642-37635-1_4_Chapter.pdf (400.16 Ko) Télécharger le fichier
Origin Files produced by the author(s)

Dates and versions

hal-01485978 , version 1 (09-03-2017)

Licence

Identifiers

Cite

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⟩
65 View
76 Download

Altmetric

Share

More