{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:08:38Z","timestamp":1725484118538},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439288"},{"type":"electronic","value":"9783540456148"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45614-7_29","type":"book-chapter","created":{"date-parts":[[2007,5,17]],"date-time":"2007-05-17T04:45:28Z","timestamp":1179377128000},"page":"511-530","source":"Crossref","is-referenced-by-count":0,"title":["Property Dependent Abstraction of Control Structure for Software Verification"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Firley","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ursula","family":"Goltz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,9]]},"reference":[{"key":"29_CR1","doi-asserted-by":"crossref","unstructured":"Alexander Asteroth, Christel Baier, and Ulrich A\u00dfmann. Model checking with formula-dependent abstract models. In Computer Aided Verification (CAV\u2019 01), 2001.","DOI":"10.1007\/3-540-44585-4_14"},{"key":"29_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1007\/3-540-56922-7_4","volume-title":"Proceedings of Computer Aided Verification (CAV\u2019 93)","author":"F. Balarin","year":"1993","unstructured":"Felice Balarin and Alberto L. Sangiovanni-Vincentelli. An iterative approach to language containment. In Courcoubetis, editor, Proceedings of Computer Aided Verification (CAV\u2019 93), volume 697 of Lecture Notes in Computer Science, pages 29\u201340. Springer, 1993."},{"key":"29_CR3","doi-asserted-by":"crossref","unstructured":"Edmund M. Clarke, Orna Grumberg, and David E. Long. Model checking and abstraction. In Conference record of the Nineteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 343\u2013354. ACM Press, 1992.","DOI":"10.1145\/143165.143235"},{"key":"29_CR4","unstructured":"Edmund M. Clarke, Orna Grumberg, and Doron Peled. Model Checking. MIT Press, 1999."},{"issue":"2","key":"29_CR5","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1145\/244795.244800","volume":"19","author":"D. Dams","year":"1997","unstructured":"Dennis Dams, Orna Grumberg, and Rob Gerth. Abstract interpretation of reactive systems. ACM Transactions on Programming Languages and Systems, 19(2):253\u2013291, 1997.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"29_CR6","doi-asserted-by":"crossref","unstructured":"[HCD+99]_John Hatcliff, James C. Corbett, Matthew B. Dwyer, Stefan Sokolowski, and Hongjun Zheng. A formal study of slicing for multi-threaded programs with JVM concurrency primitives. In Proceedings of the International Symposium on Static Analysis (SAS\u2019 99), 1999.","DOI":"10.1007\/3-540-48294-6_1"},{"key":"29_CR7","unstructured":"Michael Jones and Ganesh Gopalakrishnan. Verifying transaction ordering properties in unbounded bus networks through combined deductive\/algorithmic methods. In Formal Methods in Computer-Aided Design, pages 505\u2013519, 2000."},{"key":"29_CR8","doi-asserted-by":"crossref","unstructured":"Jae-Young Jang, Shaz Qadeer, Matt Kaufmann, and Carl Pixley. Formal verification of FIRE: A case study. In Design Automation Conference, pages 173\u2013177, 1997.","DOI":"10.1145\/266021.266059"},{"key":"29_CR9","doi-asserted-by":"crossref","unstructured":"Robert P. Kurshan. Computer-Aided Verification of Coordinating Processes. Princeton University Press, 1994.","DOI":"10.1515\/9781400864041"},{"key":"29_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF01384313","volume":"6","author":"L. Loiseaux","year":"1995","unstructured":"[LGS+95]_Claire Loiseaux, Susanne Graf, Joseph Sifakis, Ahmed Bouajjani, and Saddek Bensalem. Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design, 6:1\u201335, 1995.","journal-title":"Formal Methods in System Design"},{"key":"29_CR11","doi-asserted-by":"crossref","unstructured":"Zohar Manna and Amir Pnueli. The Temporal Logic of Reactive and Concurrent Systems, Specification. Springer, 1992.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"29_CR12","doi-asserted-by":"crossref","unstructured":"[PVE+00]_John Penix, Willem Visser, Eric Engstrom, Aaron Larson, and Nicholas Weininger. Verification of time partitioning in the DEOS scheduler kernel. In International Conference on Software Engineering, pages 488\u2013497, 2000.","DOI":"10.1145\/337180.337364"},{"key":"29_CR13","volume-title":"Technical Report TR ST 00 3","author":"N. Sidorova","year":"2000","unstructured":"Natalia Sidorova and Martin Steffen. Verification of a wireless atm medium access protocol. Technical Report TR ST 00 3, University of Kiel, Germany, May 2000."},{"key":"29_CR14","volume-title":"Technical Report CS-2000-03","author":"K. Yorav","year":"2000","unstructured":"Karen Yorav and Orna Grumberg. Static analysis for state-space reductions preserving temporal logics. Technical Report CS-2000-03, Technion, Israel, 2000."}],"container-title":["Lecture Notes in Computer Science","FME 2002:Formal Methods\u2014Getting IT Right"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45614-7_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T04:05:07Z","timestamp":1556424307000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45614-7_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439288","9783540456148"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-45614-7_29","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}