{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T04:09:03Z","timestamp":1747541343501,"version":"3.40.5"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319153162"},{"type":"electronic","value":"9783319153179"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-15317-9_20","type":"book-chapter","created":{"date-parts":[[2015,1,29]],"date-time":"2015-01-29T06:05:37Z","timestamp":1422511537000},"page":"327-345","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Algorithmic Verification of Procedural Programs in the Presence of Code Variability"],"prefix":"10.1007","author":[{"given":"Siavash","family":"Soleimanifard","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dilian","family":"Gurov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,1,30]]},"reference":[{"key":"20_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Arenas, M., Barcelo, P., Etessami, K., Immerman, N., Libkin, L.: First-order and temporal logics for nested words. In: LICS, pp. 151\u2013160 (2007)","DOI":"10.1109\/LICS.2007.19"},{"key":"20_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. TOPLAS 27, 786\u2013818 (2005)","journal-title":"TOPLAS"},{"key":"20_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/978-3-642-11319-2_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R Alur","year":"2010","unstructured":"Alur, R., Chaudhuri, S.: Temporal reasoning for procedural programs. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 45\u201360. Springer, Heidelberg (2010)"},{"key":"20_CR4","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 of nested calls and returns. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 467\u2013481. Springer, Heidelberg (2004)"},{"key":"20_CR5","doi-asserted-by":"crossref","unstructured":"Andersen, H.: Partial model checking. In: LICS, pp. 398\u2013407 (1995)","DOI":"10.1109\/LICS.1995.523274"},{"key":"20_CR6","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"Rudiments of $$\\mu $$-Calculus","author":"A Arnold","year":"2001","unstructured":"Arnold, A., Niwi\u0144ski, D.: Rudiments of $$\\mu $$-Calculus. Studies in Logic and the Foundations of Mathematics, vol. 146. Elsevier, Amsterdam (2001)"},{"key":"20_CR7","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: The SLAM project: debugging system software via static analysis. In: POPL, pp. 1\u20133 (2002)","DOI":"10.1145\/503272.503274"},{"key":"20_CR8","unstructured":"Beki\u010d, H.: Definable operators in general algebras, and the theory of automata and flowcharts. Technical report, IBM Laboratory (1967)"},{"key":"20_CR9","unstructured":"Cleaveland, R., Parrow, J., Steffen, B.: A semantics based verification tool for finite state systems. In: IFIP WG6.1, pp. 287\u2013302 (1990)"},{"key":"20_CR10","doi-asserted-by":"crossref","unstructured":"Das, M., Lerner, S., Seigle, M.: ESP: path-sensitive program verification in polynomial time. In: PLDI, pp. 57\u201368. ACM (2002)","DOI":"10.1145\/543552.512538"},{"key":"20_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/978-3-642-54804-8_15","volume-title":"Fundamental Approaches to Software Engineering","author":"P de Carvalho Gomes","year":"2014","unstructured":"de Carvalho Gomes, P., Picoco, A., Gurov, D.: Sound control flow graph extraction from incomplete Java bytecode programs. In: Gnesi, S., Rensink, A. (eds.) FASE 2014 (ETAPS). LNCS, vol. 8411, pp. 215\u2013229. Springer, Heidelberg (2014)"},{"issue":"3","key":"20_CR12","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. TOPLAS 16(3), 843\u2013871 (1994)","journal-title":"TOPLAS"},{"issue":"7","key":"20_CR13","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. Inf. Comput. 206(7), 840\u2013868 (2008)","journal-title":"Inf. Comput."},{"key":"20_CR14","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1145\/2455.2460","volume":"32","author":"M Hennessy","year":"1985","unstructured":"Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM 32, 137\u2013161 (1985)","journal-title":"J. ACM"},{"key":"20_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-540-88194-0_11","volume-title":"Formal Methods and Software Engineering","author":"M Huisman","year":"2008","unstructured":"Huisman, M., Aktug, I., Gurov, D.: Program models for compositional verification. In: Liu, S., Araki, K. (eds.) ICFEM 2008. LNCS, vol. 5256, pp. 147\u2013166. Springer, Heidelberg (2008)"},{"key":"20_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-642-18070-5_8","volume-title":"Formal Verification of Object-Oriented Software","author":"M Huisman","year":"2011","unstructured":"Huisman, M., Gurov, D.: CVPP: a tool set for compositional verification of control\u2013flow safety properties. In: Beckert, B., March\u00e9, C. (eds.) FoVeOOS 2010. LNCS, vol. 6528, pp. 107\u2013121. Springer, Heidelberg (2011)"},{"key":"20_CR17","unstructured":"Servlet Development. Release 2 (9.0.3). http:\/\/docs.oracle.com\/cd\/A97688_16\/generic.903\/a97680\/develop.htm#1007089"},{"key":"20_CR18","unstructured":"Kiefer, S., Schwoon, S., Suwimonteerabuth, D.: Moped\u2013a model-checker for pushdown systems. http:\/\/www.informatik.uni-stuttgart.de\/fmi\/szs\/tools\/moped\/"},{"key":"20_CR19","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 $$\\mu $$-calculus. TCS 27, 333\u2013354 (1983)","journal-title":"TCS"},{"issue":"1","key":"20_CR20","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. TOPLAS 22(1), 87\u2013128 (2000)","journal-title":"TOPLAS"},{"key":"20_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/3-540-52148-8_19","volume-title":"Automatic Verification Methods for Finite State Systems","author":"KG Larsen","year":"1989","unstructured":"Larsen, K.G.: Modal specifications. In: Sifakis, J. (ed.) Automatic Verification Methods for Finite State Systems. LNCS, vol. 407, pp. 232\u2013246. Springer, Heidelberg (1989)"},{"key":"20_CR22","series-title":"Lecture Notes in Computer Science","volume-title":"Modular Specification and Verification of Object-Oriented Programs","year":"2002","unstructured":"M\u00fcller, P. (ed.): Modular Specification and Verification of Object-Oriented Programs. LNCS, vol. 2262. Springer, Heidelberg (2002)"},{"key":"20_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-40213-5_1","volume-title":"Fundamentals of Software Engineering","author":"J Rot","year":"2013","unstructured":"Rot, J., de Boer, F., Bonsangue, M.: Unbounded allocation in bounded heaps. In: Arbab, F., Sirjani, M. (eds.) FSEN 2013. LNCS, vol. 8161, pp. 1\u201316. Springer, Heidelberg (2013)"},{"key":"20_CR24","unstructured":"Soleimanifard, S., Gurov, D.: Algorithmic verification of procedural programs in the presence of code variability. Technical report, KTH (2013). http:\/\/urn.kb.se\/resolve?urn=urn:nbn:se:kth:diva-128950"},{"key":"20_CR25","doi-asserted-by":"publisher","unstructured":"Soleimanifard, S., Gurov, D., Huisman, M.: Procedure-modular specification and verification of temporal safety properties. Softw. Syst. Model. (2013). doi:10.1007\/s10270-013-0321-0","DOI":"10.1007\/s10270-013-0321-0"},{"key":"20_CR26","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3550-5","volume-title":"Modal and Temporal Logics of Processes","author":"C Stirling","year":"2001","unstructured":"Stirling, C.: Modal and Temporal Logics of Processes. Springer, New York (2001)"}],"container-title":["Lecture Notes in Computer Science","Formal Aspects of Component Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-15317-9_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,17]],"date-time":"2025-05-17T23:23:42Z","timestamp":1747524222000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-15317-9_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319153162","9783319153179"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-15317-9_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"30 January 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}