Bounded Model Checking of Recursive Programs with Pointers in KReportar como inadecuado




Bounded Model Checking of Recursive Programs with Pointers in K - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

1 Alexandru Ioan Cuza University of Iași Romania 2 CWI - Centrum voor Wiskunde en Informatica 3 LIACS - Leiden Institute of Advanced Computer Science Leiden

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.

Keywords : pushdown systems model checking the $\mathbb{K}$ framework





Autor: Irina Asăvoae - Frank Boer - Marcello Bonsangue - Dorel Lucanu - Jurriaan Rot -

Fuente: https://hal.archives-ouvertes.fr/



DESCARGAR PDF




Documentos relacionados