{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:12:45Z","timestamp":1725549165143},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642120282"},{"type":"electronic","value":"9783642120299"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-12029-9_17","type":"book-chapter","created":{"date-parts":[[2010,3,7]],"date-time":"2010-03-07T19:56:48Z","timestamp":1267991808000},"page":"233-247","source":"Crossref","is-referenced-by-count":6,"title":["Automatic Cross Validation of Multiple Specifications: A Case Study"],"prefix":"10.1007","author":[{"given":"Carlo","family":"Ghezzi","sequence":"first","affiliation":[]},{"given":"Andrea","family":"Mocci","sequence":"additional","affiliation":[]},{"given":"Guido","family":"Salvaneschi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","volume-title":"Program Development in Java: Abstraction, Specification and Object-Oriented Design","author":"J.V. Guttag","year":"2001","unstructured":"Guttag, J.V., Liskov, B.: Program Development in Java: Abstraction, Specification and Object-Oriented Design. Addison-Wesley, Reading (2001)"},{"key":"17_CR2","volume-title":"Fundamentals of Software Engineering","author":"C. Ghezzi","year":"2002","unstructured":"Ghezzi, C., Jazayeri, M., Mandrioli, D.: Fundamentals of Software Engineering. Prentice Hall PTR, Upper Saddle River (2002)"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"Harel, D., Gery, E.: Executable object modeling with statecharts. In: ICSE 1996: 18th International Conference on Software Engineering (1996)","DOI":"10.1109\/ICSE.1996.493420"},{"key":"17_CR4","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/978-1-4615-5229-1_12","volume-title":"Behavioral Specifications of Businesses and Systems","author":"G.T. Leavens","year":"1999","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: JML: A notation for detailed design. In: Behavioral Specifications of Businesses and Systems, pp. 175\u2013188. Kluwer, Dordrecht (1999)"},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"Guttag, J.V., Horning, J.J.: The algebraic specification of abstract data types. Acta Informatica\u00a010(1) (1978)","DOI":"10.1007\/BF00260922"},{"key":"17_CR6","unstructured":"Ernst, M.D.: Dynamically Discovering Likely Program Invariants. Ph.D. thesis, University of Washington, Seattle, Washington (August 2000)"},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"Ghezzi, C., Mocci, A., Monga, M.: Synthesizing intensional behavior models by graph transformation. In: ICSE 2009: Proc. of 31st Int. Conf. on Soft. Eng. (2009)","DOI":"10.1109\/ICSE.2009.5070542"},{"issue":"8","key":"17_CR8","doi-asserted-by":"publisher","first-page":"526","DOI":"10.1109\/TSE.2007.70705","volume":"33","author":"J. Henkel","year":"2007","unstructured":"Henkel, J., Reichenbach, C., Diwan, A.: Discovering documentation for Java container classes. IEEE Trans. Software Eng.\u00a033(8), 526\u2013543 (2007)","journal-title":"IEEE Trans. Software Eng."},{"key":"17_CR9","unstructured":"Baresi, L., Ghezzi, C., Mocci, A., Monga, M.: Using graph transformation systems to specify and verify data abstractions. In: Proc. of GT-VMT 2008 (2008)"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Inf. Comput.\u00a098(2)","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"17_CR11","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"D. Jackson","year":"2006","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2006)"},{"key":"17_CR12","series-title":"Lecture Notes in Computer Science","volume-title":"CASL Reference Manual","year":"2004","unstructured":"Mosses, P.D. (ed.): CASL Reference Manual. LNCS (IFIP Series), vol.\u00a02960. Springer, Heidelberg (2004)"},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"Doong, R., Frankl, P.G.: The ASTOOT approach to testing object-oriented programs. ACM Trans. on Soft. Eng. and Meth.\u00a03(2) (1994)","DOI":"10.1145\/192218.192221"},{"key":"17_CR14","series-title":"EATCS Monographs in TCS","volume-title":"Fundamentals of Algebraic Graph Transformation","author":"H. Ehrig","year":"2005","unstructured":"Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic Graph Transformation. EATCS Monographs in TCS. Springer, Heidelberg (2005)"},{"key":"17_CR15","unstructured":"Spy Checker Website (2009), http:\/\/home.dei.polimi.it\/mocci\/spy\/check\/"},{"key":"17_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"17_CR17","doi-asserted-by":"crossref","unstructured":"Chechik, M., Devereux, B., Easterbrook, S., Gurfinkel, A.: Multi-valued symbolic model-checking. ACM Tr. Softw. Eng. Methodol.\u00a012(4) (2003)","DOI":"10.1145\/990010.990011"},{"key":"17_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/978-3-540-71209-1_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Mossakowski","year":"2007","unstructured":"Mossakowski, T., Maeder, C., L\u00fcttich, K.: The heterogeneous tool set, hets. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 519\u2013522. Springer, Heidelberg (2007)"},{"issue":"2","key":"17_CR19","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s00766-005-0024-3","volume":"11","author":"S. Uchitel","year":"2006","unstructured":"Uchitel, S., Chatley, R., Kramer, J., Magee, J.: Goal and scenario validation: a fluent combination. Requir. Eng.\u00a011(2), 123\u2013137 (2006)","journal-title":"Requir. Eng."},{"key":"17_CR20","volume-title":"ICSM 2004","author":"I. Ivkovic","year":"2004","unstructured":"Ivkovic, I., Kontogiannis, K.: Tracing evolution changes of software artifacts through model synchronization. In: ICSM 2004. IEEE Computer Society, Los Alamitos (2004)"}],"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-12029-9_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,23]],"date-time":"2020-11-23T21:46:51Z","timestamp":1606168011000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-12029-9_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642120282","9783642120299"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-12029-9_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}