{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T19:41:53Z","timestamp":1725565313855},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540223429"},{"type":"electronic","value":"9783540278139"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-27813-9_10","type":"book-chapter","created":{"date-parts":[[2010,9,14]],"date-time":"2010-09-14T04:57:57Z","timestamp":1284440277000},"page":"122-134","source":"Crossref","is-referenced-by-count":0,"title":["Using Interface Refinement to Integrate Formal Verification into the Design Cycle"],"prefix":"10.1007","author":[{"given":"Jacob","family":"Chang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sergey","family":"Berezin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David L.","family":"Dill","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"10_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/BFb0031808","volume-title":"Formal Methods in Computer-Aided Design","author":"C. Barrett","year":"1996","unstructured":"Barrett, C., Dill, D.L., Levitt, J.: Validity checking for combinations of theories with equality. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 187\u2013201. Springer, Heidelberg (1996)"},{"key":"10_CR2","unstructured":"Bj0rner, N., Browne, A., Colon, M., Finkbeiner, B., Manna, Z., Sipma, H., Uribe, T.: Verifying temporal properties of reactive systems: A STeP tutorial. Formal Methods in System Design (1999)"},{"key":"10_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1007\/3540539816_73","volume-title":"TAPSOFT \u201991. Proceedings of the International Joint Conference on Theory and Practice of Software Development, Brighton, UK, April 8-12, 1991","author":"E. Brinksma","year":"1991","unstructured":"Brinksma, E., Jonsson, B., Orava, F.: Refining interfaces of communicating systems. In: Abramsky, S. (ed.) TAPSOFT 1991, CCPSD 1991, and ADC-Talks 1991. LNCS, vol.\u00a0494, pp. 297\u2013312. Springer, Heidelberg (1991)"},{"key":"10_CR4","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-02880-3","volume-title":"Program Design Calculi: Proceedings of the 1992 Marktoberdorf International Summer School","author":"M. Broy","year":"1993","unstructured":"Broy, M.: Interaction refinement\u2014the easy way. In: Program Design Calculi: Proceedings of the 1992 Marktoberdorf International Summer School, Springer, Heidelberg (1993)"},{"key":"10_CR5","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"J.R. Burch","year":"1994","unstructured":"Burch, J.R., Dill, D.L.: Automatic verification of pipelined microprocessor control. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, Springer, Heidelberg (1994)"},{"key":"10_CR6","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1109\/LICS.1989.39190","volume-title":"Fourth Annual Symposium, on Logic in Computer Science","author":"E.M. Clarke","year":"1989","unstructured":"Clarke, E.M., Long, D.E., McMillan, K.L.: Compositional model checking. In: Fourth Annual Symposium, on Logic in Computer Science, June 1989, pp. 353\u2013362. IEEE Comput. Soc. Press, Washington (1989)"},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/BFb0084784","volume-title":"CONCUR \u201992","author":"R. Gerth","year":"1992","unstructured":"Gerth, R., Kupiter, R., Segers, J.: Interface refinement in reactive systems. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol.\u00a0630, pp. 77\u201393. Springer, Heidelberg (1992)"},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/3-540-49519-3_21","volume-title":"Formal Methods in Computer-Aided Design","author":"D. Greve","year":"1998","unstructured":"Greve, D.: Symbolic simulation of the JEM1 microprocessor. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol.\u00a01522, pp. 321\u2013333. Springer, Heidelberg (1998)"},{"issue":"3","key":"10_CR9","doi-asserted-by":"publisher","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O. Grumberg","year":"1994","unstructured":"Grumberg, O., Long, D.E.: Model checking and modular verification. ACM Transactions on Programming Languages and Systems\u00a016(3), 843\u2013871 (1994)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/3-540-44585-4_40","volume-title":"Computer Aided Verification","author":"R. Jhala","year":"2001","unstructured":"Jhala, R., McMillan, K.L.: Microarchitecture verification by compositional model checking. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 396\u2013410. Springer, Heidelberg (2001)"},{"key":"10_CR11","unstructured":"Kroning, D.: Formal Verification of Pipelined Microprocessors. PhD thesis, Saarland University (2001)"},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"Kurki-Suonio, R.: Component and interface refinement in closed-system specifications. In: World Congress on Formal Methods (1), pp. 134\u2013154 (1999)","DOI":"10.1007\/3-540-48119-2_10"},{"key":"10_CR13","first-page":"657","volume-title":"Information Processing","author":"L. Lamport","year":"1983","unstructured":"Lamport, L.: What good is temporal logic? In: Mason, R.E.A. (ed.) Information Processing, pp. 657\u2013668. Elsevier, Amsterdam (1983)"},{"key":"10_CR14","unstructured":"Long, D.E.: Model Checking, Abstraction, and Compositional Verification. PhD thesis, Carnegie Mellon University (1993)"},{"key":"10_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028738","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"1998","unstructured":"McMillan, K.L.: Verification of an implementation of Tomasulo\u2019s algorithm by compositional model checking. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, Springer, Heidelberg (1998)"},{"key":"10_CR16","unstructured":"McMillan, K.L.: Getting started with SMV (March 1999)"},{"key":"10_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/3-540-44798-9_17","volume-title":"Correct Hardware Design and Verification Methods","author":"K.L. McMillan","year":"2001","unstructured":"McMillan, K.L.: Parameterized verification of the flash cache coherence protocol by compositional model checking. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol.\u00a02144, pp. 179\u2013195. Springer, Heidelberg (2001)"},{"key":"10_CR18","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1006\/inco.2001.2967","volume":"170","author":"A. Rensink","year":"2001","unstructured":"Rensink, A., Gorrieri, R.: Vertical implementation. Information and Computation\u00a0170, 95\u2013133 (2001)","journal-title":"Information and Computation"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-27813-9_10.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T03:27:27Z","timestamp":1620012447000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-27813-9_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540223429","9783540278139"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-27813-9_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}