{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:56:04Z","timestamp":1725558964753},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642142949"},{"type":"electronic","value":"9783642142956"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14295-6_45","type":"book-chapter","created":{"date-parts":[[2010,7,8]],"date-time":"2010-07-08T22:36:09Z","timestamp":1278628569000},"page":"527-542","source":"Crossref","is-referenced-by-count":18,"title":["Learning Component Interfaces with May and Must Abstractions"],"prefix":"10.1007","author":[{"given":"Rishabh","family":"Singh","sequence":"first","affiliation":[]},{"given":"Dimitra","family":"Giannakopoulou","sequence":"additional","affiliation":[]},{"given":"Corina","family":"P\u0103s\u0103reanu","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"45_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Cern\u00fd, P., Madhusudan, P., Nam, W.: Synthesis of interface specifications for java classes. In: POPL, pp. 98\u2013109 (2005)","DOI":"10.1145\/1047659.1040314"},{"key":"45_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.A., Mang, F.Y.C., Qadeer, S., Rajamani, S.K., Tasiran, S.: Mocha: Modularity in model checking. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 521\u2013525. Springer, Heidelberg (1998)"},{"key":"45_CR3","doi-asserted-by":"crossref","unstructured":"Ammons, G., Bod\u00edk, R., Larus, J.R.: Mining specifications. In: POPL, pp. 4\u201316 (2002)","DOI":"10.1145\/565816.503275"},{"issue":"2","key":"45_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. Inf. Comput.\u00a075(2), 87\u2013106 (1987)","journal-title":"Inf. Comput."},{"key":"45_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":"45_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E. Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"key":"45_CR7","first-page":"238","volume-title":"POPL","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238\u2013252. ACM, New York (1977)"},{"key":"45_CR8","doi-asserted-by":"crossref","unstructured":"Das, M., Lerner, S., Seigle, M.: Esp: Path-sensitive program verification in polynomial time. In: PLDI, pp. 57\u201368 (2002)","DOI":"10.1145\/543552.512538"},{"key":"45_CR9","doi-asserted-by":"crossref","unstructured":"de Alfaro, L., Godefroid, P., Jagadeesan, R.: Three-valued abstractions of games: Uncertainty, but with precision. In: LICS (2004)","DOI":"10.1109\/LICS.2004.1319611"},{"key":"45_CR10","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":"45_CR11","doi-asserted-by":"crossref","unstructured":"Foster, J.S., Terauchi, T., Aiken, A.: Flow-sensitive type qualifiers. In: PLDI, pp. 1\u201312 (2002)","DOI":"10.1145\/512529.512531"},{"key":"45_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1007\/978-3-642-00593-0_7","volume-title":"Fundamental Approaches to Software Engineering","author":"D. Giannakopoulou","year":"2009","unstructured":"Giannakopoulou, D., Pasareanu, C.S.: Interface generation and compositional verification in javapathfinder. In: Chechik, M., Wirsing, M. (eds.) FASE 2009. LNCS, vol.\u00a05503, pp. 94\u2013108. Springer, Heidelberg (2009)"},{"key":"45_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"426","DOI":"10.1007\/3-540-44685-0_29","volume-title":"CONCUR 2001 - Concurrency Theory","author":"P. Godefroid","year":"2001","unstructured":"Godefroid, P., Huth, M., Jagadeesan, R.: Abstraction-based model checking using modal transition systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol.\u00a02154, p. 426. Springer, Heidelberg (2001)"},{"key":"45_CR14","series-title":"Lecture Notes in Computer Science","first-page":"275","volume-title":"Computer Aided Verification","author":"P. Godefroid","year":"2003","unstructured":"Godefroid, P., Huth, M., Jagadeesan, R.: A game-based framework for ctl counterexamples and 3-valued abstraction-refinement. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 275\u2013287. Springer, Heidelberg (2003)"},{"key":"45_CR15","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Nori, A.V., Rajamani, S.K., Tetali, S.D.: Compositional may-must program analysis: Unleashing the power of alternation. In: POPL (2010)","DOI":"10.1145\/1706299.1706307"},{"key":"45_CR16","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R.: Permissive interfaces. In: ESEC\/SIGSOFT FSE, pp. 31\u201340 (2005)","DOI":"10.1145\/1081706.1081713"},{"key":"45_CR17","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL, pp. 232\u2013244 (2004)","DOI":"10.1145\/964001.964021"},{"key":"45_CR18","unstructured":"Jones, C.B.: Specification and design of (parallel) programs. In: IFIP Congress, pp. 321\u2013332 (1983)"},{"key":"45_CR19","doi-asserted-by":"crossref","unstructured":"Lee, D., Yannakakis, M.: Online minimization of transition systems. In: ACM Symposium on Theory of Computing (1992)","DOI":"10.1145\/129712.129738"},{"key":"45_CR20","first-page":"264","volume-title":"STOC","author":"D. Lee","year":"1992","unstructured":"Lee, D., Yannakakis, M.: Online minimization of transition systems (extended abstract). In: STOC, pp. 264\u2013274. ACM, New York (1992)"},{"key":"45_CR21","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice Hall, New York (1989)"},{"key":"45_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"435","DOI":"10.1007\/10722167_33","volume-title":"Computer Aided Verification","author":"K.S. Namjoshi","year":"2000","unstructured":"Namjoshi, K.S., Kurshan, R.P.: Syntactic program transformations for automatic abstraction. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 435\u2013449. Springer, Heidelberg (2000)"},{"key":"45_CR23","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: In transition from global to modular temporal reasoning about programs. In: Logics and models of concurrent systems, pp. 123\u2013144 (1985)","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"45_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-540-69611-7_16","volume-title":"Practical Aspects of Declarative Languages","author":"A. Podelski","year":"2006","unstructured":"Podelski, A., Rybalchenko, A.: ARMC: The logical choice for software model checking with abstraction refinement. In: Hanus, M. (ed.) PADL 2007. LNCS, vol.\u00a04354, pp. 245\u2013259. Springer, Heidelberg (2006)"},{"issue":"2","key":"45_CR25","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1006\/inco.1993.1021","volume":"103","author":"R.L. Rivest","year":"1993","unstructured":"Rivest, R.L., Schapire, R.E.: Inference of finite automata using homing sequences. Inf. Comput.\u00a0103(2), 299\u2013347 (1993)","journal-title":"Inf. Comput."},{"key":"45_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-540-74061-2_5","volume-title":"Static Analysis","author":"S. Shoham","year":"2007","unstructured":"Shoham, S., Grumberg, O.: Compositional verification and 3-valued abstractions join forces. In: Riis Nielson, H., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol.\u00a04634, pp. 69\u201386. Springer, Heidelberg (2007)"},{"key":"45_CR27","doi-asserted-by":"crossref","unstructured":"Tkachuk, O., Dwyer, M.B.: Adapting side effects analysis for modular program model checking. In: ESEC \/ SIGSOFT FSE, pp. 188\u2013197 (2003)","DOI":"10.1145\/940071.940097"},{"key":"45_CR28","doi-asserted-by":"crossref","unstructured":"Whaley, J., Martin, M.C., Lam, M.S.: Automatic extraction of object-oriented component interfaces. In: ISSTA, pp. 218\u2013228 (2002)","DOI":"10.1145\/566172.566212"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14295-6_45.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:50:41Z","timestamp":1606186241000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14295-6_45"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642142949","9783642142956"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14295-6_45","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}