{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T16:27:38Z","timestamp":1746289658722},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642005923"},{"type":"electronic","value":"9783642005930"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-00593-0_7","type":"book-chapter","created":{"date-parts":[[2009,3,27]],"date-time":"2009-03-27T10:26:08Z","timestamp":1238149568000},"page":"94-108","source":"Crossref","is-referenced-by-count":28,"title":["Interface Generation and Compositional Verification in JavaPathfinder"],"prefix":"10.1007","author":[{"given":"Dimitra","family":"Giannakopoulou","sequence":"first","affiliation":[]},{"given":"Corina S.","family":"P\u0103s\u0103reanu","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Cerny, P., Madhusudan, P., Nam, W.: Synthesis of interface specifications for Java classes. In: Proceedings of POPL 2005, pp. 98\u2013109 (2005)","DOI":"10.1145\/1040305.1040314"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1007\/BFb0028774","volume-title":"Computer Aided Verification","author":"R. Alur","year":"1998","unstructured":"Alur, R., Henzinger, T., Mang, F., Qadeer, S., Rajamani, S., Tasiran, S.: MOCHA: Modularity in Model Checking. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 521\u2013525. Springer, Heidelberg (1998)"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Ammons, G., Bodik, R., Larus, J.R.: Mining specifications. In: Proceedings of ACM POPL 2002, pp. 4\u201316 (2002)","DOI":"10.1145\/503272.503275"},{"issue":"2","key":"7_CR4","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0890-5401(87)90052-6","volume":"75","author":"D. Angluin","year":"1987","unstructured":"Angluin, D.: Learning regular sets from queries and counterexamples. Information and Computation\u00a075(2), 87\u2013106 (1987)","journal-title":"Information and Computation"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/978-3-540-73368-3_4","volume-title":"Computer Aided Verification","author":"D. Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Singh, V.: Algorithms for Interface Synthesis. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 4\u201319. Springer, Heidelberg (2007)"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/3-540-36577-X_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J.M. Cobleigh","year":"2003","unstructured":"Cobleigh, J.M., Giannakopoulou, D., Pasareanu, C.S.: Learning Assumptions for Compositional Verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 331\u2013346. Springer, Heidelberg (2003)"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/3-540-45927-8_19","volume-title":"Programming Languages and Systems","author":"C. Flanagan","year":"2002","unstructured":"Flanagan, C., Freund, S.N., Qadeer, S.: Thread-Modular Verification for Shared-Memory Programs. In: Le M\u00e9tayer, D. (ed.) ESOP 2002. LNCS, vol.\u00a02305, pp. 262\u2013277. Springer, Heidelberg (2002)"},{"key":"7_CR8","first-page":"3","volume-title":"Proceedings of ASE 2002","author":"D. Giannakopoulou","year":"2002","unstructured":"Giannakopoulou, D., Pasareanu, C.S., Barringer, H.: Assumption Generation for Software Component Verification. In: Proceedings of ASE 2002, pp. 3\u201312. IEEE Computer Society, Los Alamitos (2002)"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/3-540-46002-0_25","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Groce","year":"2002","unstructured":"Groce, A., Peled, D., Yannakakis, M.: Adaptive Model Checking. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, p. 357. Springer, Heidelberg (2002)"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R.: Permissive Interfaces. In: Proceedings of ESEC\/SIGSOFT FSE 2005, pp. 31\u201340 (2005)","DOI":"10.1145\/1081706.1081713"},{"key":"7_CR11","unstructured":"Java PathFinder, http:\/\/javapathfinder.sourceforge.net"},{"key":"7_CR12","first-page":"321","volume-title":"Information Processing 1983: Proceedings of the IFIP 9th World Congress, IFIP","author":"C.B. Jones","year":"1983","unstructured":"Jones, C.B.: Specification and Design of (Parallel) Programs. In: Information Processing 1983: Proceedings of the IFIP 9th World Congress, IFIP, pp. 321\u2013332. North Holland, Amsterdam (1983)"},{"key":"7_CR13","volume-title":"Concurrency: State Models & Java Programs","author":"J. Magee","year":"1999","unstructured":"Magee, J., Kramer, J.: Concurrency: State Models & Java Programs. John Wiley & Sons, Chichester (1999)"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Margaria, T., Raffelt, H., Steffen, B., Leucker, M.: The LearnLib in FMICS-jETI. In: Proceedings of ICECCS 2007 (2007)","DOI":"10.1109\/ICECCS.2007.43"},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"Mehlitz, P.: Trust Your Model - Verifying Aerospace System Models with Java Pathfinder. In: IEEE\/Aero (2008)","DOI":"10.1109\/AERO.2008.4526573"},{"key":"7_CR16","doi-asserted-by":"crossref","unstructured":"Pasareanu, C.S., Giannakopoulou, D., Gheorghiu Bobaru, M., Cobleigh, J.M., Barringer, H.: Learning to Divide-and-Conquer: Applying the L* Algorithm to Automate Assume-Guarantee Reasoning. In: FMSD (January 2008)","DOI":"10.1007\/s10703-008-0049-6"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: In Transition from Global to Modular Temporal Reasoning about Programs. In: Logic and Models of Concurrent Systems, vol.\u00a013, pp. 123\u2013144 (1984)","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","first-page":"188","volume-title":"Fast Software Encryption","author":"O. Tkachuk","year":"2003","unstructured":"Tkachuk, O., Dwyer, M.B.: Adapting side effects analysis for modular program model checking. In: Johansson, T. (ed.) FSE 2003. LNCS, vol.\u00a02887, pp. 188\u2013197. Springer, Heidelberg (2003)"},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"Whaley, J., Martin, M.C., Lam, M.S.: Automatic extraction of object-oriented component interfaces. In: Proceedings of ISSTA 2002, pp. 218\u2013228 (2002)","DOI":"10.1145\/566172.566212"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-00593-0_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T04:19:55Z","timestamp":1558239595000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-00593-0_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642005923","9783642005930"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-00593-0_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}