{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T07:31:54Z","timestamp":1725521514423},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540938996"},{"type":"electronic","value":"9783540939009"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-93900-9_14","type":"book-chapter","created":{"date-parts":[[2008,12,15]],"date-time":"2008-12-15T09:35:59Z","timestamp":1229333759000},"page":"136-150","source":"Crossref","is-referenced-by-count":5,"title":["Reducing Behavioural to Structural Properties of Programs with Procedures"],"prefix":"10.1007","author":[{"given":"Dilian","family":"Gurov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marieke","family":"Huisman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"14_CR1","first-page":"151","volume-title":"Logic in Computer Science (LICS 2007)","author":"R. Alur","year":"2007","unstructured":"Alur, R., Arenas, M., Barcelo, P., Etessami, K., Immerman, N., Libkin, L.: First-order and temporal logics for nested words. In: Logic in Computer Science (LICS 2007), Washington, DC, USA, pp. 151\u2013160. IEEE Computer Society Press, Los Alamitos (2007)"},{"key":"14_CR2","doi-asserted-by":"publisher","first-page":"786","DOI":"10.1145\/1075382.1075387","volume":"27","author":"R. Alur","year":"2005","unstructured":"Alur, R., Benedikt, M., Etessami, K., Godefroid, P., Reps, T., Yannakakis, M.: Analysis of recursive state machines. ACM TOPLAS\u00a027, 786\u2013818 (2005)","journal-title":"ACM TOPLAS"},{"key":"14_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1007\/978-3-540-24730-2_35","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Alur","year":"2004","unstructured":"Alur, R., Etessami, K., Madhusudan, P.: A temporal logic for nested calls and returns. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 467\u2013481. Springer, Heidelberg (2004)"},{"key":"14_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/3-540-54233-7_126","volume-title":"Automata, Languages and Programming","author":"A. Bouajjani","year":"1991","unstructured":"Bouajjani, A., Fernandez, J.C., Graf, S., Rodriguez, C., Sifakis, J.: Safety for branching time semantics. In: Leach Albert, J., Monien, B., Rodr\u00edguez-Artalejo, M. (eds.) ICALP 1991. LNCS, vol.\u00a0510, pp. 76\u201392. Springer, Heidelberg (1991)"},{"key":"14_CR5","first-page":"545","volume-title":"Handbook of Process Algebra","author":"O. Burkart","year":"2000","unstructured":"Burkart, O., Caucal, D., Moller, F., Steffen, B.: Verification on infinite structures. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, pp. 545\u2013623. North-Holland, Amsterdam (2000)"},{"issue":"2","key":"14_CR6","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1093\/logcom\/12.2.255","volume":"12","author":"M. Dam","year":"2002","unstructured":"Dam, M., Gurov, D.: \u03bc-calculus with explicit points and approximations. Journal of Logic and Computation\u00a012(2), 43\u201357 (2002)","journal-title":"Journal of Logic and Computation"},{"key":"14_CR7","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1109\/LICS.2004.1319628","volume-title":"Nineteenth Annual IEEE Symposium on Logic in Computer Science (LICS 2004)","author":"D. Dams","year":"2004","unstructured":"Dams, D., Namjoshi, K.S.: The existence of finite abstractions for branching time model checking. In: Nineteenth Annual IEEE Symposium on Logic in Computer Science (LICS 2004), pp. 335\u2013344. IEEE Computer Society Press, Los Alamitos (2004)"},{"key":"14_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/10722167_20","volume-title":"Computer Aided Verification","author":"J. Esparza","year":"2000","unstructured":"Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient algorithms for model checking pushdown systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 232\u2013247. Springer, Heidelberg (2000)"},{"issue":"3","key":"14_CR9","doi-asserted-by":"publisher","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O. Grumberg","year":"1994","unstructured":"Grumberg, O., Long, D.: Model checking and modular verification. ACM TOPLAS\u00a016(3), 843\u2013871 (1994)","journal-title":"ACM TOPLAS"},{"key":"14_CR10","unstructured":"Gurov, D., Huisman, M.: From behavioural to structural properties: A tool web interface, \n                    \n                      http:\/\/www.csc.kth.se\/~dilian\/Projects\/CVPP\/beh2struct.php"},{"key":"14_CR11","unstructured":"Gurov, D., Huisman, M.: Reducing behavioural to structural properties of programs with procedures. Technical Report TRITA-CSC-TCS 2007:3, KTH Royal Institute of Technology, Stockholm, 35 pages (2007), \n                    \n                      http:\/\/www.csc.kth.se\/~dilian\/Papers\/techrep-07-3.pdf"},{"issue":"7","key":"14_CR12","doi-asserted-by":"publisher","first-page":"840","DOI":"10.1016\/j.ic.2008.03.003","volume":"206","author":"D. Gurov","year":"2008","unstructured":"Gurov, D., Huisman, M., Sprenger, C.: Compositional verification of sequential programs with procedures. Information and Computation\u00a0206(7), 840\u2013868 (2008)","journal-title":"Information and Computation"},{"key":"14_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/978-3-540-88194-0_11","volume-title":"International Conference on Formal Engineering Methods (ICFEM 2008)","author":"M. Huisman","year":"2008","unstructured":"Huisman, M., Aktug, I., Gurov, D.: Program models for compositional verification. In: International Conference on Formal Engineering Methods (ICFEM 2008). LNCS, vol.\u00a05256, pp. 147\u2013166. Springer, Heidelberg (2008)"},{"key":"14_CR14","unstructured":"Huisman, M., Gurov, D.: Composing modal properties of programs with procedures. In: Formal Foundations of Embedded Software and Component-Based Software Architectures (FESCA 2007). Electronic Notes in Theoretical Computer Science (to appear, 2008)"},{"key":"14_CR15","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional \u03bc-calculus. Theoretical Computer Science\u00a027, 333\u2013354 (1983)","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"14_CR16","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/0096-0551(93)90003-J","volume":"19","author":"U. Reddy","year":"1993","unstructured":"Reddy, U., Kamin, S.: On the power of abstract interpretation. Computer Languages\u00a019(2), 79\u201389 (1993)","journal-title":"Computer Languages"},{"issue":"1-2","key":"14_CR17","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1016\/j.scico.2005.02.009","volume":"58","author":"T. Reps","year":"2005","unstructured":"Reps, T., Schwoon, S., Jha, S., Melski, D.: Weighted pushdown systems and their application to interprocedural dataflow analysis. Science of Computer Programming\u00a058(1-2), 206\u2013263 (2005)","journal-title":"Science of Computer Programming"},{"issue":"1","key":"14_CR18","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1145\/353323.353382","volume":"3","author":"F.B. Schneider","year":"2000","unstructured":"Schneider, F.B.: Enforceable security policies. ACM Trans. Infinite Systems Security\u00a03(1), 30\u201350 (2000)","journal-title":"ACM Trans. Infinite Systems Security"},{"key":"14_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/3-540-45931-6_26","volume-title":"Foundations of Software Science and Computation Structures","author":"U. Sch\u00f6pp","year":"2002","unstructured":"Sch\u00f6pp, U., Simpson, A.K.: Verifying temporal properties using explicit approximants: Completeness for context-free processes. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol.\u00a02303, pp. 372\u2013386. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-93900-9_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,4]],"date-time":"2019-03-04T10:54:24Z","timestamp":1551696864000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-93900-9_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540938996","9783540939009"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-93900-9_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}