{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T07:02:52Z","timestamp":1743145372075,"version":"3.40.3"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319014173"},{"type":"electronic","value":"9783319014180"}],"license":[{"start":{"date-parts":[[2013,8,14]],"date-time":"2013-08-14T00:00:00Z","timestamp":1376438400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2013,8,14]],"date-time":"2013-08-14T00:00:00Z","timestamp":1376438400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-01418-0_2","type":"book-chapter","created":{"date-parts":[[2013,9,18]],"date-time":"2013-09-18T10:39:50Z","timestamp":1379500790000},"page":"17-36","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Efficient Refinement Strategy Exploiting Component Properties in a CEGAR Process"],"prefix":"10.1007","author":[{"given":"Syed Hussein S.","family":"Alwi","sequence":"first","affiliation":[]},{"given":"C\u00e9cile","family":"Braunstein","sequence":"additional","affiliation":[]},{"given":"Emmanuelle","family":"Encrenaz","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2013,8,14]]},"reference":[{"key":"2_CR1","unstructured":"The VIS Group: VIS: A system for verification and synthesis, In: Alur, R., Henzinger, T.A. (eds.) Proceedings of the 8th International Conference, CAV \u201996, New Brunswick. LNCS, vol. 1102, pp. 428\u2013432. Springer, Berlin\/Heidelberg (1996)"},{"key":"2_CR2","volume-title":"Computer Aided Verification (CAV \u201997), Haifa. LNCS","author":"S. Graf","year":"1997","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) Computer Aided Verification (CAV \u201997), Haifa. LNCS, vol. 1254. Springer, London, Springer Berlin Heidelberg (1997)"},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: CAV\u201900, Chicago. LNCS (2000)","DOI":"10.1007\/10722167_15"},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"Ball, T., Cook, B., Levin, V., Rajamani, S.K.: SLAM and static driver verifier: Technology transfer of formal methods inside microsoft. In: 4th International Conference on Integrated Formal Methods, Canterbury, vol. 2999, pp. 1\u201320. Springer (2004)","DOI":"10.1007\/978-3-540-24756-2_1"},{"issue":"5\u20136","key":"2_CR5","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"D. Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker blast: Applications to software engineering. Int. J. Softw. Tools Technol. Trans. 9(5\u20136), 505\u2013525 (2007)","journal-title":"Int. J. Softw. Tools Technol. Trans."},{"key":"2_CR6","unstructured":"Jain, H., Kroening, D., Sharygina, N., Clarke, E.: VCEGAR: Verilog counterexample guided abstraction refinement. In: TACAS\u201907, Braga, 2007"},{"key":"2_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10009-011-0185-y","volume":"14","author":"N. Sharygina","year":"2012","unstructured":"Sharygina, N., Tonetta, S., Tsitovich, A.: An abstraction refinement approach combining precise and approximated techniques. Int. J. Softw. Tools Technol. Trans. 14, 1\u201314 (2012)","journal-title":"Int. J. Softw. Tools Technol. Trans."},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Grumberg, O., Long, D.E.: Model checking and modular verification. In: International Conference on Concurency Theory, Amsterdam, vol. 527, pp. 250\u2013263. Springer, Berlin\/Heidelberg (1991)","DOI":"10.1007\/3-540-54430-5_93"},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Qadeer, S., Rajamani, S.K.: You assume, we guarantee: Methodology and case studies. In: CAV \u201998, Vancouver, vol. 1427, pp. 440\u2013451. Springer, Berlin\/Heidelberg (1998)","DOI":"10.1007\/BFb0028765"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"Xie, F., Browne, J.C.: Verified systems by composition from verified components, in ESEC\/FSE 2003. In: 11th ACM SIGSOFT Symposium on Foundations of Software Engineering Conference, Helsinki, pp. 227\u2013286. ACM (2003)","DOI":"10.1145\/940071.940109"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"Li, J., Sun, X., Xie, F., Song, X.: Component-based abstraction refinement. In: 10th International Conference on Software Reuse (ICSR), Beijing, pp. 39\u201351. Springer (2008)","DOI":"10.1007\/978-3-540-68073-4_4"},{"key":"2_CR12","unstructured":"Peng, H., Mokhtari, Y., Tahar, S.: Environment synthesis for compositional model checking. In: ICCD \u201902: 20th International Conference on Computer Design, Freiburg, pp. 70\u201375. IEEE Computer Society (2002)"},{"key":"2_CR13","unstructured":"Schickel, M., Nimbler, V., Braun, M., Eveking, H.: On consistency and completeness of property-sets: Exploiting the property-based design process. In: FDL \u201906: Forum on Specification and Design Languages, Darmstadt (2006)"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"Nguyen, M.D., Wedler, M., Stoffel, D., Kunz, W.: Formal hardware\/software co-verification by interval property checking with abstraction. In: Design Automation Conference (DAC\u201911), San Diego 2011","DOI":"10.1145\/2024724.2024843"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Braunstein, C., Encrenaz, E.: Using CTL formulae as component abstraction in a design verification flow. In: ACSD, Bratislava, pp. 80\u201389. IEEE Computer Society (2007)","DOI":"10.1109\/ACSD.2007.76"},{"key":"2_CR16","unstructured":"Bara, A.: Abstraction de Composant pour la V\u00e9rification par Model-Checking, M\u00e9moire de Dipl\u00f4me Universitaire OMP \u2013 LIP6-SOC, (2008)"},{"issue":"5","key":"2_CR17","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E.M. Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512\u20131542 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"Belnap, N.: A useful four-valued logic. In: Modern Uses of Multiple-Valued Logic, pp. 8\u201337. Springer, Berlin\/Heidelberg (1977)","DOI":"10.1007\/978-94-010-1161-7_2"},{"key":"2_CR19","unstructured":"Braunstein, C.: Conception Incr\u00e9mentale, V\u00e9rification de Composants Mat\u00e9riels et M\u00e9thode d\u2019abstraction pour la V\u00e9rification de Syst\u00e8mes Int\u00e9gr\u00e9s sur Puce. Ph.D. thesis, Universit\u00e9 Pierre et Marie Curie, LIP6-SOC (2007)"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"Pardo, S., Hachtel, G.: Incremental CTL model checking using BDD subsetting. In: DAC \u201998: 35th Design Automation Conference, San Francisco, pp. 457\u2013462. ACM (1998)","DOI":"10.1145\/277044.277171"},{"key":"2_CR21","doi-asserted-by":"crossref","unstructured":"Pardo, S., Hachtel, G.: Automatic abstraction technique for propositional mu-Calculus model checking. In: CAV \u201997, Haifa, vol. 1254, pp. 12\u201323. Springer, (1997)","DOI":"10.1007\/3-540-63166-6_5"},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"Purandare, M., Wahl, T., Kroening, D.: Strengthening properties using abstraction refinement. In: Proceedings of DATE \u201909, Nice, pp. 1692\u20131697. ACM (2009)","DOI":"10.1109\/DATE.2009.5090935"}],"container-title":["Lecture Notes in Electrical Engineering","Models, Methods, and Tools for Complex Chip Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-01418-0_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,7]],"date-time":"2023-02-07T16:22:19Z","timestamp":1675786939000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-01418-0_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,8,14]]},"ISBN":["9783319014173","9783319014180"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-01418-0_2","relation":{},"ISSN":["1876-1100","1876-1119"],"issn-type":[{"type":"print","value":"1876-1100"},{"type":"electronic","value":"1876-1119"}],"subject":[],"published":{"date-parts":[[2013,8,14]]},"assertion":[{"value":"14 August 2013","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}