{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T11:28:24Z","timestamp":1742383704420},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540691471"},{"type":"electronic","value":"9783540691495"}],"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-69149-5_36","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T16:07:43Z","timestamp":1218557263000},"page":"337-346","source":"Crossref","is-referenced-by-count":2,"title":["Scalable Software Model Checking Using Design for Verification"],"prefix":"10.1007","author":[{"given":"Tevfik","family":"Bultan","sequence":"first","affiliation":[]},{"given":"Aysu","family":"Betin-Can","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"doi-asserted-by":"crossref","unstructured":"Betin-Can, A., Bultan, T.: Interface-based specification and verification of concurrency controllers. Proc. SoftMC, ENTCS, vol.\u00a089 (2003)","key":"36_CR1","DOI":"10.1016\/S1571-0661(05)80007-6"},{"doi-asserted-by":"crossref","unstructured":"Betin-Can, A., Bultan, T.: Verifiable concurrent programming using concurrency controllers. In: Proc. 19th IEEE Int. Conf. on ASE, pp. 248\u2013257 (2004)","key":"36_CR2","DOI":"10.1109\/ASE.2004.1342742"},{"doi-asserted-by":"crossref","unstructured":"Betin-Can, A., Bultan, T.: Verifiable web services with hierarchichal interfaces. In: Proc. IEEE Int. Conf. on Web Services, pp. 85\u201394 (2005)","key":"36_CR3","DOI":"10.1109\/ICWS.2005.128"},{"doi-asserted-by":"crossref","unstructured":"Betin-Can, A., Bultan, T., Fu, X.: Design for verification for asynchronously communicating web services. In: Proc. 14th WWW Conf. pp. 750\u2013759 (2005)","key":"36_CR4","DOI":"10.1145\/1060745.1060853"},{"doi-asserted-by":"crossref","unstructured":"Betin-Can, A., Bultan, T., Lindvall, M., Topp, S., Lux, B.: Application of design for verification with concurrency controllers to air traffic control software. In: Proc. 20th IEEE Int. Conf. on ASE (to appear, 2005)","key":"36_CR5","DOI":"10.1145\/1101908.1101914"},{"doi-asserted-by":"crossref","unstructured":"Boigelot, B., Godefroid, P., Williams, B., Wolper, P.: The power of QDDs. In: Proc. 4th Static Analysis Symp. pp. 172\u2013186 (1997)","key":"36_CR6","DOI":"10.1007\/BFb0032741"},{"doi-asserted-by":"crossref","unstructured":"Bultan, T., Fu, X., Hull, R., Su, J.: Conversation specification: A new approach to design and analysis of e-service composition. In: Proc. 12th WWW Conf. pp. 403\u2013410 (2003)","key":"36_CR7","DOI":"10.1145\/775152.775210"},{"key":"36_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/3-540-45657-0_35","volume-title":"Computer Aided Verification","author":"A. Chakrabarti","year":"2002","unstructured":"Chakrabarti, A., de Alfaro, L., Henzinger, T.A., Jurdzi\u0144ski, M., Mang, F.Y.C.: Interface compatibility checking for software modules. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 428\u2013441. Springer, Heidelberg (2002)"},{"key":"36_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/978-3-540-24851-4_21","volume-title":"ECOOP 2004 \u2013 Object-Oriented Programming","author":"R. DeLine","year":"2004","unstructured":"DeLine, R., Fahndrich, M.: Typestates for objects. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol.\u00a03086, pp. 465\u2013490. Springer, Heidelberg (2004)"},{"unstructured":"Dennis, G.: TSAFE: Building a trusted computing base for air traffic control software, Master\u2019s Thesis (2003)","key":"36_CR10"},{"doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for java. In: Proc. POPL, pp. 234\u2013245 (2002)","key":"36_CR11","DOI":"10.1145\/512529.512558"},{"doi-asserted-by":"crossref","unstructured":"Fu, X., Bultan, T., Su, J.: Analysis of interacting BPEL web services. In: Proc. 13th WWW Conf. pp. 621\u2013630 (2004)","key":"36_CR12","DOI":"10.1145\/988672.988756"},{"doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Model checking for programming languages using VeriSoft. In: Proc. POPL, January 1997, pp. 174\u2013186 (1997)","key":"36_CR13","DOI":"10.1145\/263699.263717"},{"doi-asserted-by":"crossref","unstructured":"Godefroid, P., Colby, C., Jagadeesan, L.: Automatically closing open reactive programs. In: Proc. PLDI, June 1998, pp. 345\u2013357 (1998)","key":"36_CR14","DOI":"10.1145\/277652.277754"},{"issue":"5","key":"36_CR15","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker spin. IEEE Transactions on Software Eng.\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Transactions on Software Eng."},{"unstructured":"Java API for XML messaging (JAXM). http:\/\/java.sun.com\/xml\/jaxm\/","key":"36_CR16"},{"unstructured":"Mehlitz, P.C., Penix, J.: Design for verification using design patterns to build reliable systems. In: Proc. Work. on Component-Based Soft. Eng. (2003)","key":"36_CR17"},{"key":"36_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/3-540-48234-2_14","volume-title":"Theoretical and Practical Aspects of SPIN Model Checking","author":"C.S. Pasareanu","year":"1999","unstructured":"Pasareanu, C.S., Dwyer, M.B., Huth, M.: Assume guarantee model checking of software: A comparative case study. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol.\u00a01680, pp. 168\u2013183. Springer, Heidelberg (1999)"},{"key":"36_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1007\/3-540-45314-8_23","volume-title":"Fundamental Approaches to Software Engineering","author":"N. Sharygina","year":"2001","unstructured":"Sharygina, N., Browne, J.C., Kurshan, R.P.: A formal object-oriented analysis for software reliability: Design for verification. In: Hussmann, H. (ed.) ETAPS 2001 and FASE 2001. LNCS, vol.\u00a02029, pp. 318\u2013332. Springer, Heidelberg (2001)"},{"doi-asserted-by":"crossref","unstructured":"Tkachuk, O., Dwyer, M.B.: Adapting side-effects analysis for modular program model checking. In: Proc. ASE, pp. 116\u2013129 (2003)","key":"36_CR20","DOI":"10.1145\/940071.940097"},{"doi-asserted-by":"crossref","unstructured":"Tkachuk, O., Dwyer, M.B., Pasareanu, C.: Automated environment generation for software model checking. In: Proc. ESEC\/FSE, pp. 188\u2013197 (2003)","key":"36_CR21","DOI":"10.1109\/ASE.2003.1240300"},{"issue":"2","key":"36_CR22","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1023\/A:1022920129859","volume":"10","author":"W. Visser","year":"2003","unstructured":"Visser, W., Havelund, K., Brat, G., Park, S.: Model checking programs. Automated Software Engineering Journal\u00a010(2), 203\u2013232 (2003)","journal-title":"Automated Software Engineering Journal"},{"doi-asserted-by":"crossref","unstructured":"Wilhelm, R., Sagiv, M., Reps, T.: Shape analysis. In: Proc. 9th Int. Conf. on Compiler Construction, pp. 1\u201317 (2000)","key":"36_CR23","DOI":"10.1007\/3-540-46423-9_1"},{"key":"36_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/11513988_40","volume-title":"Computer Aided Verification","author":"T. Yavuz-Kahveci","year":"2005","unstructured":"Yavuz-Kahveci, T., Bartzis, C., Bultan, T.: Action language verifier, extended. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 413\u2013417. Springer, Heidelberg (2005)"},{"doi-asserted-by":"crossref","unstructured":"Yavuz-Kahveci, T., Bultan, T.: Specification, verification, and synthesis of concurrency control components. In: Proc. ISSTA, pp. 169\u2013179 (2002)","key":"36_CR25","DOI":"10.1145\/566172.566199"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69149-5_36","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T07:43:11Z","timestamp":1557733391000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69149-5_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540691471","9783540691495"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69149-5_36","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}