{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T21:04:18Z","timestamp":1760043858668,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642252709"},{"type":"electronic","value":"9783642252716"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-25271-6_10","type":"book-chapter","created":{"date-parts":[[2011,12,14]],"date-time":"2011-12-14T20:56:11Z","timestamp":1323896171000},"page":"184-203","source":"Crossref","is-referenced-by-count":17,"title":["Compositional Algorithmic Verification of Software Product Lines"],"prefix":"10.1007","author":[{"given":"Ina","family":"Schaefer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dilian","family":"Gurov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Siavash","family":"Soleimanifard","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"10_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/978-3-642-02408-5_2","volume-title":"Theory and Practice of Model Transformations","author":"S. Apel","year":"2009","unstructured":"Apel, S., Janda, F., Trujillo, S., K\u00e4stner, C.: Model Superimposition in Software Product Lines. In: Paige, R.F. (ed.) ICMT 2009. LNCS, vol.\u00a05563, pp. 4\u201319. Springer, Heidelberg (2009)"},{"issue":"6","key":"10_CR2","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1109\/TSE.2004.23","volume":"30","author":"D. Batory","year":"2004","unstructured":"Batory, D., Sarvela, J., Rauschmayer, A.: Scaling Step-Wise Refinement. IEEE Trans. Software Eng.\u00a030(6), 355\u2013371 (2004)","journal-title":"IEEE Trans. Software Eng."},{"issue":"3","key":"10_CR3","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"},{"key":"10_CR4","first-page":"258","volume-title":"Automated Software Engineering (ASE 2004)","author":"C. Blundell","year":"2004","unstructured":"Blundell, C., Fisler, K., Krishnamurthi, S., van Hentenryck, P.: Parameterized Interfaces for Open System Verification of Product Lines. In: Automated Software Engineering (ASE 2004), pp. 258\u2013267. IEEE, Los Alamitos (2004)"},{"key":"10_CR5","first-page":"335","volume-title":"International Conference on Software Engineering (ICSE 2010)","author":"A. Classen","year":"2010","unstructured":"Classen, A., Heymans, P., Schobbens, P., Legay, A., Raskin, J.: Model Checking Lots of Systems: Efficient Verification of Temporal Properties in Software Product Lines. In: International Conference on Software Engineering (ICSE 2010), pp. 335\u2013344. IEEE, Los Alamitos (2010)"},{"key":"10_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1007\/11561347_28","volume-title":"Generative Programming and Component Engineering","author":"K. Czarnecki","year":"2005","unstructured":"Czarnecki, K., Antkiewicz, M.: Mapping Features to Models: A Template Approach Based on Superimposed Variants. In: Gl\u00fcck, R., Lowry, M. (eds.) GPCE 2005. LNCS, vol.\u00a03676, pp. 422\u2013437. Springer, Heidelberg (2005)"},{"key":"10_CR7","volume-title":"Generative Programming: Methods, Tools, and Applications","author":"K. Czarnecki","year":"2000","unstructured":"Czarnecki, K., Eisenecker, U.W.: Generative Programming: Methods, Tools, and Applications. Addison-Wesley, Reading (2000)"},{"key":"10_CR8","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1109\/SPLC.2008.45","volume-title":"Software Product Line Conference (SPLC 2008)","author":"A. Fantechi","year":"2008","unstructured":"Fantechi, A., Gnesi, S.: Formal Modeling for Product Families Engineering. In: Software Product Line Conference (SPLC 2008), pp. 193\u2013202. IEEE, Los Alamitos (2008)"},{"key":"10_CR9","volume-title":"Designing Software Product Lines with UML","author":"H. Gomaa","year":"2004","unstructured":"Gomaa, H.: Designing Software Product Lines with UML. Addison Wesley, Reading (2004)"},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-540-68863-1_8","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"A. Gruler","year":"2008","unstructured":"Gruler, A., Leucker, M., Scheidemann, K.: Modeling and model checking software product lines. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol.\u00a05051, pp. 113\u2013131. Springer, Heidelberg (2008)"},{"issue":"3","key":"10_CR11","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 Transactions on Programming Languages and Systems\u00a016(3), 843\u2013871 (1994)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"10_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/978-3-540-93900-9_14","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D. Gurov","year":"2009","unstructured":"Gurov, D., Huisman, M.: Reducing behavioural to structural properties of programs with procedures. In: Jones, N.D., M\u00fcller-Olm, M. (eds.) VMCAI 2009. LNCS, vol.\u00a05403, pp. 136\u2013150. Springer, Heidelberg (2009)"},{"issue":"7","key":"10_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. Information and Computation\u00a0206(7), 840\u2013868 (2008)","journal-title":"Information and Computation"},{"key":"10_CR14","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1109\/SPLC.2008.25","volume-title":"Software Product Line Conference (SPLC 2008)","author":"\u00d8. Haugen","year":"2008","unstructured":"Haugen, \u00d8., M\u00f8ller-Pedersen, B., Oldevik, J., Olsen, G., Svendsen, A.: Adding Standardized Variability to Domain Specific Languages. In: Software Product Line Conference (SPLC 2008), pp. 139\u2013148. IEEE, Los Alamitos (2008)"},{"key":"10_CR15","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.\u00a06528, pp. 107\u2013121. Springer, Heidelberg (2011)"},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"Kang, K., Lee, J., Donohoe, P.: Feature-Oriented Project Line Engineering. IEEE Software\u00a019(4) (2002)","DOI":"10.1109\/MS.2002.1020288"},{"key":"10_CR17","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"},{"key":"10_CR18","first-page":"269","volume-title":"Automated Software Engineering (ASE 2009)","author":"K. Lauenroth","year":"2009","unstructured":"Lauenroth, K., Pohl, K., Toehning, S.: Model checking of domain artifacts in product line engineering. In: Automated Software Engineering (ASE 2009), pp. 269\u2013280. IEEE, Los Alamitos (2009)"},{"key":"10_CR19","unstructured":"Leavens, G., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., M\u00fcller, P., Kiniry, J., Chalin, P.: JML Reference Manual, Department of Computer Science, Iowa State University (February 2007), \n                    \n                      http:\/\/www.jmlspecs.org"},{"issue":"1","key":"10_CR20","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/s10515-010-0075-7","volume":"18","author":"J. Liu","year":"2011","unstructured":"Liu, J., Basu, S., Lutz, R.R.: Compositional model checking of software product lines using variation point obligations. Autom. Softw. Eng.\u00a018(1), 39\u201376 (2011)","journal-title":"Autom. Softw. Eng."},{"key":"10_CR21","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1109\/SPLC.2008.44","volume-title":"Software Product Line Conference (SPLC 2008)","author":"N. Noda","year":"2008","unstructured":"Noda, N., Kishi, T.: Aspect-Oriented Modeling for Variability Management. In: Software Product Line Conference (SPLC 2008), pp. 213\u2013222. IEEE, Los Alamitos (2008)"},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"P\u00e9rez, J., D\u00edaz, J., Soria, C.C., Garbajosa, J.: Plastic Partial Components: A solution to support variability in architectural components. In: WICSA\/ECSA, pp. 221\u2013230 (2009)","DOI":"10.1109\/WICSA.2009.5290808"},{"key":"10_CR23","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-28901-1","volume-title":"Software Product Line Engineering - Foundations, Principles, and Techniques","author":"K. Pohl","year":"2005","unstructured":"Pohl, K., B\u00f6ckle, G., van der Linden, F.: Software Product Line Engineering - Foundations, Principles, and Techniques. Springer, Heidelberg (2005)"},{"key":"10_CR24","unstructured":"Requirement Elicitation, Deliverable 5.1 of project FP7-231620 (HATS) (August 2009), \n                    \n                      http:\/\/www.hats-project.eu"},{"key":"10_CR25","unstructured":"Schwoon, S.: Model-Checking Pushdown Systems. PhD thesis, Technische Universit\u00e4t M\u00fcnchen (2002)"},{"key":"10_CR26","doi-asserted-by":"crossref","unstructured":"Soleimanifard, S., Gurov, D., Huisman, M.: Procedure\u2013modular verification of control flow safety properties. In: Workshop on Formal Techniques for Java Programs, FTfJP 2010 (2010)","DOI":"10.1145\/1924520.1924525"},{"key":"10_CR27","unstructured":"Soleimanifard, S., Gurov, D., Huisman, M.: Promover: Modular verification of temporal safety properties. In: Software Engineering and Formal Methods, SEFM 2011 (to appear,2011)"},{"key":"10_CR28","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, Heidelberg (2001)"},{"issue":"7","key":"10_CR29","doi-asserted-by":"publisher","first-page":"537","DOI":"10.1109\/TSE.2005.84","volume":"31","author":"R. Ommering van","year":"2005","unstructured":"van Ommering, R.: Software reuse in product populations. IEEE Trans. Software Eng.\u00a031(7), 537\u2013550 (2005)","journal-title":"IEEE Trans. Software Eng."},{"key":"10_CR30","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1109\/SPLINE.2007.23","volume-title":"Software Product Line Conference (SPLC 2007)","author":"M. V\u00f6lter","year":"2007","unstructured":"V\u00f6lter, M., Groher, I.: Product Line Implementation using Aspect-Oriented and Model-Driven Software Development. In: Software Product Line Conference (SPLC 2007), pp. 233\u2013242. IEEE, Los Alamitos (2007)"},{"key":"10_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/978-3-540-24667-1_10","volume-title":"Software Product-Family Engineering","author":"T. Ziadi","year":"2004","unstructured":"Ziadi, T., H\u00eblou\u00ebt, L., J\u00e9z\u00e9quel, J.-M.: Towards a UML Profile for Software Product Lines. In: van der Linden, F.J. (ed.) PFE 2003. LNCS, vol.\u00a03014, pp. 129\u2013139. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Components and Objects"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-25271-6_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,21]],"date-time":"2019-04-21T20:57:09Z","timestamp":1555880229000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-25271-6_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642252709","9783642252716"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-25271-6_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}