{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T07:12:13Z","timestamp":1725520333139},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540881933"},{"type":"electronic","value":"9783540881940"}],"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-88194-0_11","type":"book-chapter","created":{"date-parts":[[2008,10,17]],"date-time":"2008-10-17T14:56:21Z","timestamp":1224255381000},"page":"147-166","source":"Crossref","is-referenced-by-count":8,"title":["Program Models for Compositional Verification"],"prefix":"10.1007","author":[{"given":"Marieke","family":"Huisman","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Irem","family":"Aktug","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dilian","family":"Gurov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"11_CR1","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"},{"issue":"3","key":"11_CR2","doi-asserted-by":"publisher","first-page":"217","DOI":"10.3233\/JCS-2001-9303","volume":"9","author":"F. Besson","year":"2001","unstructured":"Besson, F., Jensen, T., Le M\u00e9tayer, D., Thorn, T.: Model checking security properties of control flow graphs. J. of Computer Security\u00a09(3), 217\u2013250 (2001)","journal-title":"J. of Computer Security"},{"issue":"1","key":"11_CR3","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1145\/640128.604137","volume":"38","author":"A. Bouajjani","year":"2003","unstructured":"Bouajjani, A., Esparza, J., Touili, T.: A generic approach to the static analysis of concurrent programs with procedures. SIGPLAN Notes\u00a038(1), 62\u201373 (2003)","journal-title":"SIGPLAN Notes"},{"key":"11_CR4","unstructured":"Bretagne, E., El Marouani, A., Girard, P., Lanet, J.-L.: PACAP purse and loyalty specification. Technical Report V 0.4, Gemplus (2000)"},{"key":"11_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)"},{"key":"11_CR6","first-page":"287","volume-title":"International Symposium on Protocol Specification, Testing and Verification","author":"R. Cleaveland","year":"1990","unstructured":"Cleaveland, R., Parrow, J., Steffen, B.: A semantics based verification tool for finite state systems. In: International Symposium on Protocol Specification, Testing and Verification, pp. 287\u2013302. North-Holland Publishing Co., Amsterdam (1990)"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1007\/11691372_35","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Esparza","year":"2006","unstructured":"Esparza, J., Kiefer, S., Schwoon, S.: Abstraction refinement with Craig interpolation and symbolic pushdown systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 489\u2013503. Springer, Heidelberg (2006)"},{"key":"11_CR8","first-page":"1","volume-title":"Principles of programming languages (POPL 2000)","author":"J. Esparza","year":"2000","unstructured":"Esparza, J., Podelski, A.: Efficient algorithms for pre* and post* on interprocedural parallel flow graphs. In: Principles of programming languages (POPL 2000), pp. 1\u201311. ACM Press, New York (2000)"},{"issue":"3","key":"11_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":"11_CR10","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 (2007)"},{"issue":"7","key":"11_CR11","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":"11_CR12","unstructured":"Huisman, M., Aktug, I., Gurov, D.: Flow graph behaviour for multi-threaded applications (2007), ftp:\/\/ftp-sop.inria.fr\/everest\/Marieke.Huisman\/mt.pdf"},{"key":"11_CR13","unstructured":"Kiefer, S., Schwoon, S., Suwimonteerabuth, D.: http:\/\/www.informatik.uni-stuttgart.de\/fmi\/szs\/tools\/moped\/"},{"key":"11_CR14","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":"1","key":"11_CR15","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1145\/345099.345104","volume":"22","author":"O. Kupferman","year":"2000","unstructured":"Kupferman, O., Vardi, M.: An automata-theoretic approach to modular model checking. ACM TOPLAS\u00a022(1), 87\u2013128 (2000)","journal-title":"ACM TOPLAS"},{"key":"11_CR16","unstructured":"Lindholm, T., Yellin, F.: The JavaTM Virtual Machine Specification, 2nd edn. Sun Microsystems, Inc. (1999)"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"Manson, J., Pugh, W., Adve, S.: The Java memory model. In: Principles of Programming Languages (2005)","DOI":"10.1145\/1040305.1040336"},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"M\u00e9ndez, M., Navas, J., Hermenegildo, M.V.: An efficient, parametric fixpoint algorithm for analysis of Java bytecode. In: Huisman, M., Spoto, F. (eds.) Bytecode 2007, pp. 51\u201366 (2007)","DOI":"10.1016\/j.entcs.2007.02.060"},{"key":"11_CR19","unstructured":"Obdr\u017e\u00e1lek, J.: Model checking Java using pushdown systems. In: Proceedings of FTfJP 2002, Malaga, Available as Technical Report NIII-R0204, Computing Science Department, University of Nijmegen (June 2002)"},{"key":"11_CR20","unstructured":"Polansky, D.: Implementation of the model checker for pushdown systems and alternation-free mu-calculus. Master\u2019s thesis, FI MU Brno (2000)"},{"key":"11_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-540-31980-1_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Qadeer","year":"2005","unstructured":"Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 93\u2013107. Springer, Heidelberg (2005)"},{"issue":"2","key":"11_CR22","doi-asserted-by":"publisher","first-page":"416","DOI":"10.1145\/349214.349241","volume":"22","author":"G. Ramalingam","year":"2000","unstructured":"Ramalingam, G.: Context-sensitive synchronization-sensitive analysis is undecidable. ACM TOPLAS\u00a022(2), 416\u2013430 (2000)","journal-title":"ACM TOPLAS"},{"key":"11_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1007\/978-3-540-31980-1_35","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Suwimonteerabuth","year":"2005","unstructured":"Suwimonteerabuth, D., Schwoon, S., Esparza, J.: jMoped: A Java bytecode checker based on Moped. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 541\u2013545. Springer, Heidelberg (2005)"},{"key":"11_CR24","unstructured":"Vall\u00e9e-Rai, R., Hendren, L., Sundaresan, V., Lam, P., Gagnon, E., Co, P.: Soot - a Java Optimization Framework. In: CASCON 1999, pp. 125\u2013135 (1999)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-88194-0_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,14]],"date-time":"2019-05-14T19:08:09Z","timestamp":1557860889000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-88194-0_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540881933","9783540881940"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-88194-0_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}