{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:52:10Z","timestamp":1725486730235},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642376344"},{"type":"electronic","value":"9783642376351"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-37635-1_4","type":"book-chapter","created":{"date-parts":[[2013,4,10]],"date-time":"2013-04-10T21:30:45Z","timestamp":1365629445000},"page":"59-76","source":"Crossref","is-referenced-by-count":2,"title":["Bounded Model Checking of Recursive Programs with Pointers in K"],"prefix":"10.1007","author":[{"given":"Irina M\u0103riuca","family":"As\u0103voae","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Frank","family":"de Boer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marcello M.","family":"Bonsangue","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dorel","family":"Lucanu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jurriaan","family":"Rot","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/3-540-63141-0_10","volume-title":"CONCUR\u201997: Concurrency Theory","author":"A. Bouajjani","year":"1997","unstructured":"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.\u00a01243, pp. 135\u2013150. Springer, Heidelberg (1997)"},{"key":"4_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-540-73368-3_24","volume-title":"Computer Aided Verification","author":"A. Bouajjani","year":"2007","unstructured":"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.\u00a04590, pp. 207\u2013220. Springer, Heidelberg (2007)"},{"key":"4_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"226","DOI":"10.1007\/978-3-642-19829-8_15","volume-title":"SBM 2010","author":"M. Bonsangue","year":"2011","unstructured":"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\u00e3o, A. (eds.) SBMF 2010. LNCS, vol.\u00a06527, pp. 226\u2013241. Springer, Heidelberg (2011)"},{"key":"4_CR4","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1016\/S1571-0661(05)82534-4","volume":"71","author":"S. Eker","year":"2002","unstructured":"Eker, S., Meseguer, J., Sridharanarayanan, A.: The Maude LTL Model Checker. Electr. Notes Theor. Comput. Sci.\u00a071, 162\u2013187 (2002)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Ellison, C., Ro\u015fu, G.: An Executable Formal Semantics of C with Applications. In: Field, J., Hicks, M. (eds.) POPL 2012, pp. 533\u2013544. ACM (2012)","DOI":"10.1145\/2103621.2103719"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/3-540-44585-4_30","volume-title":"Computer Aided Verification","author":"J. Esparza","year":"2001","unstructured":"Esparza, J., Schwoon, S.: A BDD-Based Model Checker for Recursive Programs. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 324\u2013336. Springer, Heidelberg (2001)"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Goguen, J., Lin, K., Ro\u015fu, G.: Circular Coinductive Rewriting. In: ASE 2000, pp. 123\u2013132. IEEE (2000)","DOI":"10.1109\/ASE.2000.873657"},{"key":"4_CR8","unstructured":"Kidd, N., Reps, T., Melski, D., Lal, A.: WPDS++: A C++ Library for Weighted Pushdown Systems (2005), \n                  \n                    http:\/\/www.cs.wisc.edu\/wpis\/wpds++"},{"key":"4_CR9","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1145\/256167.256195","volume":"19","author":"D. Kozen","year":"1997","unstructured":"Kozen, D.: Kleene Algebra with Tests. ACM Trans. Program. Lang. Syst.\u00a019, 427\u2013443 (1997)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"4_CR10","unstructured":"Maude, \n                  \n                    http:\/\/maude.cs.uiuc.edu\/"},{"issue":"2-3","key":"4_CR11","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1016\/j.tcs.2008.04.040","volume":"403","author":"J. Meseguer","year":"2008","unstructured":"Meseguer, J., Palomino, M., Mart\u00ed-Oliet, N.: Equational Abstractions. Theor. Comput. Sci.\u00a0403(2-3), 239\u2013264 (2008)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"4_CR12","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1016\/j.tcs.2006.12.018","volume":"373","author":"J. Meseguer","year":"2007","unstructured":"Meseguer, J., Ro\u015fu, G.: The Rewriting Logics Semantics Project. Theor. Comput. Sci.\u00a0373(3), 213\u2013237 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"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\u2013309. ACM (2005)","DOI":"10.1145\/1047659.1040330"},{"issue":"6","key":"4_CR14","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1016\/j.jlap.2010.03.012","volume":"79","author":"G. Ro\u015fu","year":"2010","unstructured":"Ro\u015fu, G., \u015eerb\u0103nu\u0163\u0103, T.F.: An Overview of the K Semantic Framework. J. Log. Algebr. Program.\u00a079(6), 397\u2013434 (2010)","journal-title":"J. Log. Algebr. Program."},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/978-3-642-16310-4_8","volume-title":"Rewriting Logic and Its Applications","author":"T.F. \u015eerb\u0103nu\u0163\u0103","year":"2010","unstructured":"\u015eerb\u0103nu\u0163\u0103, T.F., Ro\u015fu, G.: K-Maude: A Rewriting Based Tool for Semantics of Programming Languages. In: \u00d6lveczky, P.C. (ed.) WRLA 2010. LNCS, vol.\u00a06381, pp. 104\u2013122. Springer, Heidelberg (2010)"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"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.\u00a0104, pp. 99\u2013113 (2012)","DOI":"10.4204\/EPTCS.104.9"},{"key":"4_CR17","unstructured":"Schwoon, S.: Model-Checking Pushdown Systems. PhD thesis, Technische Universit\u00e4t M\u00fcnchen (2002)"}],"container-title":["Lecture Notes in Computer Science","Recent Trends in Algebraic Development Techniques"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-37635-1_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T21:30:36Z","timestamp":1558301436000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-37635-1_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642376344","9783642376351"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-37635-1_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}