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.
Type de document :
Communication dans un congrès
Narciso Martí-Oliet; Miguel Palomino. 21th InternationalWorkshop on Algebraic Development Techniques (WADT), Jun 2012, Salamanca, Spain. Springer, Lecture Notes in Computer Science, LNCS-7841, pp.59-76, 2013, Recent Trends in Algebraic Development Techniques. 〈10.1007/978-3-642-37635-1_4〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01485978
Contributeur : Hal Ifip <>
Soumis le : jeudi 9 mars 2017 - 15:33:41
Dernière modification le : mercredi 20 décembre 2017 - 17:42:07
Document(s) archivé(s) le : samedi 10 juin 2017 - 14:23:27

Fichier

978-3-642-37635-1_4_Chapter.pd...
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Irina Asăvoae, Frank Boer, Marcello Bonsangue, Dorel Lucanu, Jurriaan Rot. Bounded Model Checking of Recursive Programs with Pointers in K. Narciso Martí-Oliet; Miguel Palomino. 21th InternationalWorkshop on Algebraic Development Techniques (WADT), Jun 2012, Salamanca, Spain. Springer, Lecture Notes in Computer Science, LNCS-7841, pp.59-76, 2013, Recent Trends in Algebraic Development Techniques. 〈10.1007/978-3-642-37635-1_4〉. 〈hal-01485978〉

Partager

Métriques

Consultations de la notice

36

Téléchargements de fichiers

14