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.
Chapter PDF
Similar content being viewed by others
References
Bouajjani, A., Esparza, J., Maler, O.: Reachability Analysis of Pushdown Automata: Application to Model Checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 135–150. Springer, Heidelberg (1997)
Bouajjani, A., Fratani, S., Qadeer, S.: Context-Bounded Analysis of Multithreaded Programs with Dynamic Linked Structures. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 207–220. Springer, Heidelberg (2007)
Bonsangue, M., Caltais, G., Goriac, E.-I., Lucanu, D., Rutten, J., Silva, A.: A Decision Procedure for Bisimilarity of Generalized Regular Expressions. In: Davies, J., Silva, L., da Silva Simão, A. (eds.) SBMF 2010. LNCS, vol. 6527, pp. 226–241. Springer, Heidelberg (2011)
Eker, S., Meseguer, J., Sridharanarayanan, A.: The Maude LTL Model Checker. Electr. Notes Theor. Comput. Sci. 71, 162–187 (2002)
Ellison, C., Roşu, G.: An Executable Formal Semantics of C with Applications. In: Field, J., Hicks, M. (eds.) POPL 2012, pp. 533–544. ACM (2012)
Esparza, J., Schwoon, S.: A BDD-Based Model Checker for Recursive Programs. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 324–336. Springer, Heidelberg (2001)
Goguen, J., Lin, K., Roşu, G.: Circular Coinductive Rewriting. In: ASE 2000, pp. 123–132. IEEE (2000)
Kidd, N., Reps, T., Melski, D., Lal, A.: WPDS++: A C++ Library for Weighted Pushdown Systems (2005), http://www.cs.wisc.edu/wpis/wpds++
Kozen, D.: Kleene Algebra with Tests. ACM Trans. Program. Lang. Syst. 19, 427–443 (1997)
Maude, http://maude.cs.uiuc.edu/
Meseguer, J., Palomino, M., Martí-Oliet, N.: Equational Abstractions. Theor. Comput. Sci. 403(2-3), 239–264 (2008)
Meseguer, J., Roşu, G.: The Rewriting Logics Semantics Project. Theor. Comput. Sci. 373(3), 213–237 (2007)
Rinetzky, N., Bauer, J., Reps, T.W., Sagiv, S., Wilhelm, R.: A Semantics for Procedure Local Heaps and its Abstractions. In: Palsberg, J., Abadi, M. (eds.) POPL 2005, pp. 296–309. ACM (2005)
Roşu, G., Şerbănuţă, T.F.: An Overview of the K Semantic Framework. J. Log. Algebr. Program. 79(6), 397–434 (2010)
Şerbănuţă, T.F., Roşu, G.: K-Maude: A Rewriting Based Tool for Semantics of Programming Languages. In: Ölveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 104–122. Springer, Heidelberg (2010)
Rot, J., Asavoae, I.M., de Boer, F., Bonsangue, M., Lucanu, D.: Interacting via the Heap in the Presence of Recursion. In: Carbone, M., Lanese, I., Silva, A., Sokolova, A. (eds.) ICE 2012. EPTCS, vol. 104, pp. 99–113 (2012)
Schwoon, S.: Model-Checking Pushdown Systems. PhD thesis, Technische Universität München (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 IFIP International Federation for Information Processing
About this paper
Cite this paper
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: Martí-Oliet, N., Palomino, M. (eds) Recent Trends in Algebraic Development Techniques. WADT 2012. Lecture Notes in Computer Science, vol 7841. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-37635-1_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-37635-1_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-37634-4
Online ISBN: 978-3-642-37635-1
eBook Packages: Computer ScienceComputer Science (R0)