{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:54:13Z","timestamp":1725494053954},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540664994"},{"type":"electronic","value":"9783540482345"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48234-2_5","type":"book-chapter","created":{"date-parts":[[2007,10,30]],"date-time":"2007-10-30T03:58:10Z","timestamp":1193716690000},"page":"57-76","source":"Crossref","is-referenced-by-count":9,"title":["Divide, Abstract, and Model-Check"],"prefix":"10.1007","author":[{"given":"Karsten","family":"Stahl","sequence":"first","affiliation":[]},{"given":"Kai","family":"Baukus","sequence":"additional","affiliation":[]},{"given":"Yassine","family":"Lakhnech","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Stefen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[1999,8,27]]},"reference":[{"key":"5_CR1","unstructured":"A. Bouajjani, S. Bensalem, C. Loiseaux, and J. Sifakis. Property preserving simulations. In G. v. Bochmann and D. K. Probst, editors, CAV\u201992, volume663 of LNCS. Springer, 1992"},{"key":"5_CR2","unstructured":"R. Cardell-Oliver. The specification and verification of sliding window protocols. Technical Report 183, University of Cambridge, 1989."},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In 4th POPL, Los Angeles, CA. ACM, 1977.","DOI":"10.1145\/512950.512973"},{"key":"5_CR4","unstructured":"E. M. Clarke and E. A. Emerson. Synthesis of synchronisation skeletons for branching time temporal logic. In D. Kozen, editor, Workshop on Logic of Programs1981, volume 131 ofLNCS. Springer, 1981."},{"issue":"5","key":"5_CR5","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"C. E","year":"1994","unstructured":"E. Clarke, O. Grumberg, and D. Long. Model checking and abstraction. TOPLAS, 16(5):1512\u20131542, 1994.","journal-title":"TOPLAS"},{"key":"5_CR6","unstructured":"D. Dams. Abstract interpretation and partition refinement for model che cking. PhD thesis, Technical University of Eindhoven, 1996."},{"key":"5_CR7","unstructured":"D. Dams, R. Gerth, and O. Grumberg. Abstract interpretation of reactive systems: Abstractions preserving ACTL-, ECTL- and CTL-. In E.-R. Olderog, editor, Proceedings of PROCOMET\u2019 94. North-Holland, 1994."},{"key":"5_CR8","unstructured":"I. Dravapoulos, N. Pronios, A. Andritsou, I. Piveropoulos, N. Passas, D. Skyrianoglou, G. Awater, J. Kruys, N. Nikaein, A. Enout, S. Decrauzat, T. Kaltenschnee, T. Schumann, J. Meierhofer, S. Thomel, and J. Mikkonen. The Magic WAND, Deliverable 3D5, Wireless ATM MAC, Final Report, 1998."},{"key":"5_CR9","unstructured":"W.-P. de Roever, H. Langmaack, and A. Pnueli, editors. Compos\u2019 97, volume 1536of LNCS. Springer, 1998."},{"key":"5_CR10","unstructured":"G. J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1991."},{"key":"5_CR11","unstructured":"B. Jonsson. Compositional Verification of Distributed Systems. PhD thesis, University of Uppsala, 1987. Technical Report DoCS 87\/09."},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"R. Kaivola. Using compositional preorders in the verification of sliding window protocol. In O. Grumberg, editor, Proceedings of CAV\u2019 97, volume 1256 of LNCS, pages 48\u201359. Springer, 1997.","DOI":"10.1007\/3-540-63166-6_8"},{"key":"5_CR13","unstructured":"P. Kelb. Abstraktionstechniken fur Automatische Verifikationsmethoden. PhD thesis, University of Oldenburg, 1995."},{"key":"5_CR14","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/BF01934068","volume":"21","author":"D.E. Knuth","year":"1981","unstructured":"D. E. Knuth. Verification of link-level protocols. BIT, 21:31\u201336, 1981.","journal-title":"BIT"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"R. P. Kurshan. Computer-Aided Verification of Coordinating Processes, the automata theoretic approach. Princeton Series in Computer Science. Princeton University Press, 1994.","DOI":"10.1515\/9781400864041"},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and S. Bensalem. Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design, 6(1), 1995.","DOI":"10.1007\/BF01384313"},{"key":"5_CR17","unstructured":"D. E. Long. Model Checking, Abstraction, and Compositional Reasoning. PhD thesis, Carnegie Mellon, 1993."},{"issue":"2","key":"5_CR18","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"O. S","year":"1995","unstructured":"S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal veri-cation for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107\u2013125, 1995.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"J. P. Queille and J. Sifakis. Specification and verification of concurrent systems in CESAR. In Proceedings of the Fifth International Symposium on Programming, 1981.","DOI":"10.1007\/3-540-11494-7_22"},{"key":"5_CR20","unstructured":"J. L. Richier, C. Rodriguez, J. Sifakis, and J. Voiron. Verification in Xesar of the sliding window protocol. In PSTV VII. North-Holland, 1987."},{"issue":"3","key":"5_CR21","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1145\/129393.129394","volume":"14","author":"A.U. Shankar","year":"1992","unstructured":"A. U. Shankar and S. S. Lam. A stepwise refinement heuristics for protocol construction. TOPLAS, 14(3):417\u2013461, 1992.","journal-title":"TOPLAS"}],"container-title":["Lecture Notes in Computer Science","Theoretical and Practical Aspects of SPIN Model Checking"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48234-2_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,4]],"date-time":"2019-05-04T03:15:48Z","timestamp":1556939748000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48234-2_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540664994","9783540482345"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-48234-2_5","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}