{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:04:19Z","timestamp":1740096259459,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642309816"},{"type":"electronic","value":"9783642309823"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"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":[[2012]]},"DOI":"10.1007\/978-3-642-30982-3_6","type":"book-chapter","created":{"date-parts":[[2012,6,26]],"date-time":"2012-06-26T02:04:30Z","timestamp":1340676270000},"page":"192-218","source":"Crossref","is-referenced-by-count":0,"title":["Abstractions for Validation in Action"],"prefix":"10.1007","author":[{"given":"Guido","family":"de Caso","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Victor","family":"Braberman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Diego","family":"Garbervetsky","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sebastian","family":"Uchitel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"6_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., \u010cern\u1ef3, P., Madhusudan, P., Nam, W.: Synthesis of interface specifications for Java classes. In: POPL 2005, pp. 98\u2013109 (2005)","DOI":"10.1145\/1047659.1040314"},{"issue":"1","key":"6_CR2","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"R. Alur","year":"1995","unstructured":"Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T., Ho, P., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theoretical Computer Science\u00a0138(1), 3\u201334 (1995)","journal-title":"Theoretical Computer Science"},{"key":"6_CR3","unstructured":"Andersen, M., Barnett, M., Fahndrich, M., Grunkemeyer, B., King, K., Logozzo, F., Patel, V., Zuniga, D.: Code Contracts (2009), http:\/\/research.microsoft.com\/en-us\/projects\/contracts\/"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"Beckman, N., Nori, A.: Probabilistic, modular and scalable inference of typestate specifications. In: PLDI (2011)","DOI":"10.1145\/1993498.1993524"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Beschastnikh, I., Brun, Y., Sloan, S., Ernst, M.: Leveraging existing instrumentation to automatically infer invariant-constrained models. In: FSE 2011 (2011)","DOI":"10.1145\/2025113.2025151"},{"key":"6_CR6","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., Jhala, R., Majumdar, R.: The software model checker Blast. STTT\u00a09, 505\u2013525 (2007), http:\/\/www.springerlink.com\/index\/10.1007\/s10009-007-0044-z","journal-title":"STTT"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Bierhoff, K., Aldrich, J.: Plural: checking protocol compliance under aliasing. In: ICSE, pp. 971\u2013972. ACM (2008)","DOI":"10.1145\/1370175.1370213"},{"issue":"1","key":"6_CR8","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1109\/TSE.2010.98","volume":"38","author":"G. Caso de","year":"2012","unstructured":"de Caso, G., Braberman, V., Garbervetsky, D., Uchitel, S.: Automated abstractions for contract validation. IEEE Transactions on Software Engineering\u00a038(1), 141\u2013162 (2012)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"de Caso, G., Braberman, V.A., Garbervetsky, D., Uchitel, S.: Program abstractions for behaviour validation. In: Proceedings of the 33rd International Conference on Software Engineering, ICSE 2011, Waikiki, Honolulu, HI, USA, May 21-28, pp. 381\u2013390 (2011)","DOI":"10.1145\/1985793.1985846"},{"key":"6_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/978-3-540-73589-2_12","volume-title":"ECOOP 2007 \u2013 Object-Oriented Programming","author":"P. Chalin","year":"2007","unstructured":"Chalin, P., James, P.R.: Non-null References by Default in Java: Alleviating the Nullity Annotation Burden. In: Bateni, M. (ed.) ECOOP 2007. LNCS, vol.\u00a04609, pp. 227\u2013247. Springer, Heidelberg (2007)"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Dallmeier, V., Lindig, C., Wasylkowski, A., Zeller, A.: Mining object behavior with ADABU. In: Workshop on Dynamic Systems Analysis 2006 (2006)","DOI":"10.1145\/1138912.1138918"},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"Dallmeier, V., Knopp, N., Mallon, C., Hack, S., Zeller, A.: Generating test cases for specification mining. In: ISSTA 2010 (2010)","DOI":"10.1145\/1831708.1831719"},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"DeLine, R., Fahndrich, M.: Enforcing high-level protocols in low-level software. In: PLDI 2001, pp. 59\u201369 (2001)","DOI":"10.1145\/381694.378811"},{"key":"6_CR14","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1109\/TSE.2008.91","volume":"35","author":"B. Demsky","year":"2009","unstructured":"Demsky, B., Rinard, M.: Automatic extraction of heap reference properties in object-oriented programs. IEEE Transactions on Software Engineering\u00a035, 305\u2013324 (2009)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"6_CR15","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.scico.2007.01.015","volume":"69","author":"M. Ernst","year":"2007","unstructured":"Ernst, M., Perkins, J., Guo, P., McCamant, S., Pacheco, C., Tschantz, M., Xiao, C.: The Daikon system for dynamic detection of likely invariants. Science of Computer Programming\u00a069, 35\u201345 (2007), http:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S016764230700161X","journal-title":"Science of Computer Programming"},{"key":"6_CR16","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/s002360050074","volume":"34","author":"J. Esparza","year":"1997","unstructured":"Esparza, J.: Decidability of model checking for infinite-state concurrent systems. Acta Informatica\u00a034, 85\u2013107 (1997), http:\/\/www.springerlink.com\/openurl.asp?genre=article&id=doi:10.1007\/s002360050074","journal-title":"Acta Informatica"},{"key":"6_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/3-540-45251-6_29","volume-title":"FME 2001: Formal Methods for Increasing Software Productivity","author":"C. Flanagan","year":"2001","unstructured":"Flanagan, C., Leino, K.: Houdini, an Annotation Assistant for ESC\/Java. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol.\u00a02021, pp. 500\u2013517. Springer, Heidelberg (2001)"},{"key":"6_CR18","unstructured":"Gabel, M., Su, Z.: Symbolic mining of temporal specifications. In: ICSE 2008, pp. 51\u201360 (2008), http:\/\/portal.acm.org\/citation.cfm?id=1368096"},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"Ghezzi, C., Mocci, A., Monga, M.: Synthesizing intensional behavior models by graph transformation. In: ICSE 2009, pp. 430\u2013440 (2009)","DOI":"10.1109\/ICSE.2009.5070542"},{"key":"6_CR20","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., P\u0103s\u0103reanu, 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":"6_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of Abstract State Graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"6_CR22","unstructured":"Grieskamp, W., Kicillof, N., MacDonald, D., Nandan, A., Stobie, K., Wurden, F.: Model-based quality assurance of Windows protocol documentation. In: ICST 2008, pp. 502\u2013506 (2008), http:\/\/ieeexplore.ieee.org\/lpdocs\/epic03\/wrapper.htm?arnumber=4539580"},{"issue":"3","key":"6_CR23","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1145\/234426.234431","volume":"5","author":"C.L. Heitmeyer","year":"1996","unstructured":"Heitmeyer, C.L., Jeffords, R.D., Labaw, B.G.: Automated consistency checking of requirements specifications. ACM Transactions on Software Engineering and Methodology (TOSEM)\u00a05(3), 231\u2013261 (1996)","journal-title":"ACM Transactions on Software Engineering and Methodology (TOSEM)"},{"key":"6_CR24","doi-asserted-by":"crossref","unstructured":"Henzinger, T., Jhala, R., Majumdar, R.: Permissive interfaces. In: ESEC\/FSE 2005, pp. 31\u201340 (2005)","DOI":"10.1145\/1095430.1081713"},{"key":"6_CR25","unstructured":"IEEE: IEEE Standard Glossary of Software Engineering Terminology (September 1990)"},{"key":"6_CR26","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1145\/1232743.1232745","volume":"50","author":"J. Kramer","year":"2007","unstructured":"Kramer, J.: Is abstraction the key to computing? Commun. ACM\u00a050, 36\u201342 (2007), http:\/\/doi.acm.org\/10.1145\/1232743.1232745","journal-title":"Commun. ACM"},{"key":"6_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M. Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of Probabilistic Real-Time Systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 585\u2013591. Springer, Heidelberg (2011)"},{"key":"6_CR28","unstructured":"Lee, D., Yannakakis, M.: Online minimization of transition systems (extended abstract). In: STOC 1992, pp. 264\u2013274 (1992), http:\/\/portal.acm.org\/citation.cfm?doid=129712.129738"},{"key":"6_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-540-73770-4_7","volume-title":"Tests and Proofs","author":"L. Liu","year":"2007","unstructured":"Liu, L., Meyer, B., Schoeller, B.: Using Contracts and Boolean Queries to Improve the Quality of Automatic Test Generation. In: Gurevich, Y., Meyer, B. (eds.) TAP 2007. LNCS, vol.\u00a04454, pp. 114\u2013130. Springer, Heidelberg (2007)"},{"key":"6_CR30","doi-asserted-by":"crossref","unstructured":"Lorenzoli, D., Mariani, L., Pezz\u00e8, M.: Automatic generation of software behavioral models. In: ICSE 2008, pp. 501\u2013510 (2008)","DOI":"10.1145\/1368088.1368157"},{"issue":"10","key":"6_CR31","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1145\/1103845.1094818","volume":"40","author":"M. Nanda","year":"2005","unstructured":"Nanda, M., Grothoff, C., Chandra, S.: Deriving object typestates in the presence of inter-object references. ACM SIGPLAN Notices\u00a040(10), 77\u201396 (2005)","journal-title":"ACM SIGPLAN Notices"},{"key":"6_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"6_CR33","doi-asserted-by":"crossref","unstructured":"Pradel, M., Gross, T.R.: Automatic Generation of Object Usage Specifications from Large Method Traces. In: ASE 2009, pp. 371\u2013382. IEEE (November 2009), http:\/\/ieeexplore.ieee.org\/lpdocs\/epic03\/wrapper.htm?arnumber=5431756","DOI":"10.1109\/ASE.2009.60"},{"key":"6_CR34","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1109\/ICDCS.2011.28","volume-title":"Proceedings of the 2011 31st International Conference on Distributed Computing Systems, ICDCS 2011","author":"R. Sasnauskas","year":"2011","unstructured":"Sasnauskas, R., Dustmann, O.S., Kaminski, B.L., Wehrle, K., Weise, C., Kowalewski, S.: Scalable symbolic execution of distributed systems. In: Proceedings of the 2011 31st International Conference on Distributed Computing Systems, ICDCS 2011, pp. 333\u2013342. IEEE Computer Society, Washington, DC (2011), http:\/\/dx.doi.org\/10.1109\/ICDCS.2011.28"},{"issue":"1","key":"6_CR35","first-page":"157","volume":"12","author":"R. Strom","year":"1986","unstructured":"Strom, R., Yemini, S.: Typestate: A programming language concept for enhancing software reliability. IEEE TSE\u00a012(1), 157\u2013171 (1986)","journal-title":"IEEE TSE"},{"key":"6_CR36","unstructured":"Uribe, T.: Abstraction-based Deductive-algorithmic Verification of Reactive Systems. Stanford University, Dept. of Computer Science (1999)"},{"key":"6_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1007\/3-540-65306-6_21","volume-title":"Lectures on Petri Nets I: Basic Models","author":"A. Valmari","year":"1998","unstructured":"Valmari, A.: The State Explosion Problem. In: Reisig, W., Rozenberg, G. (eds.) APN 1998. LNCS, vol.\u00a01491, pp. 429\u2013528. Springer, Heidelberg (1998)"},{"key":"6_CR38","doi-asserted-by":"crossref","first-page":"44","DOI":"10.1145\/1984708.1984721","volume-title":"Proceedings of the 1st Workshop on Developing Tools as Plug-ins, TOPI 2011","author":"E. Zoppi","year":"2011","unstructured":"Zoppi, E., Braberman, V., de Caso, G., Garbervetsky, D., Uchitel, S.: Contractor.net: inferring typestate properties to enrich code contracts. In: Proceedings of the 1st Workshop on Developing Tools as Plug-ins, TOPI 2011, pp. 44\u201347. ACM, New York (2011), http:\/\/doi.acm.org\/10.1145\/1984708.1984721"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Model-Driven Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-30982-3_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,19]],"date-time":"2022-01-19T14:29:37Z","timestamp":1642602577000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-30982-3_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642309816","9783642309823"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-30982-3_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}