{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:46:16Z","timestamp":1725493576026},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540008996"},{"type":"electronic","value":"9783540365785"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36578-8_23","type":"book-chapter","created":{"date-parts":[[2007,10,27]],"date-time":"2007-10-27T03:16:11Z","timestamp":1193454971000},"page":"325-340","source":"Crossref","is-referenced-by-count":3,"title":["Model Checking Software via Abstraction of Loop Transitions"],"prefix":"10.1007","author":[{"given":"Natasha","family":"Sharygina","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"James C.","family":"Browne","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,2,28]]},"reference":[{"key":"23_CR1","doi-asserted-by":"crossref","unstructured":"T. Ball, R. Majumdar, T. Millstein and S. Rajamani, Automatic Predicate Abstraction of C Programs, In Proc. of PLDI 2001, SIGPLAN Notices, Vol. 39 (2001)","DOI":"10.1145\/378795.378846"},{"key":"23_CR2","unstructured":"B. Beizer, Software Testing Techniques, New York: Van Nostrand Reinold, (1990)"},{"key":"23_CR3","doi-asserted-by":"crossref","unstructured":"J.J. Chilenski and S.P. Miller, Applicability of modified conditional coverage to software testing, Software Engineering Journal, (1994) 193\u2013200","DOI":"10.1049\/sej.1994.0025"},{"key":"23_CR4","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, O. Grumberg, and D. Long. Model checking and abstraction. In Proceedings POPL 92: Principles of Programming Languages, (1992) 343\u2013354","DOI":"10.1145\/143165.143235"},{"key":"23_CR5","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for the static analysis of programs by construction of approximation of fixpoints. In Proc. of POPL\u201977, (1977) 238\u2013252","DOI":"10.1145\/512950.512973"},{"key":"23_CR6","unstructured":"D. Dams, O. Grumberg, and R. Gerth. Abstract interpretation of reactive systems: abstractions preserving ACTL*, ECTL*, and CTL*. In Proceedings of PROCOMET 94: Programming Concepts, Methods, and Calculi, (1994) 561\u2013581"},{"key":"23_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Construction of abstract state graphs with PVS","author":"S. Graf","year":"1997","unstructured":"S. Graf and H. Saidi, Construction of abstract state graphs with PVS. In Proceedings of CAV 1997, LNCS 1254 (1997) 72\u201383"},{"key":"23_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1007\/3-540-61474-5_94","volume-title":"COSPAN","author":"R. Hardin","year":"1996","unstructured":"R. Hardin, Z. Har'EL, and R.P. Kurshan, COSPAN, In Proceedings of CAV 1996, LNCS 1102, (1996) 423\u2013427"},{"key":"23_CR9","unstructured":"M.S. Hecht, Flow Analysis of Computer Programs, NY: Elsevier-N. Holland (1977)"},{"key":"23_CR10","volume-title":"Design and Validation of Computer Protocols","author":"J. Holzmann","year":"1991","unstructured":"J. Holzmann, Design and Validation of Computer Protocols, Pr. Hall, NJ (1991)"},{"key":"23_CR11","unstructured":"Kapoor, C., and Tesar, D.: A Reusable Operational Software Architecture for Advanced Robotics (OSCAR), The University of Texas at Austin, DOE Grant No. DE-FG01 94EW37966 (1998)"},{"key":"23_CR12","volume-title":"Computer-Aided Verification of Coordinating Processes-The Automata Theoretic Approach","author":"R. Kurshan","year":"1994","unstructured":"Kurshan, R., Computer-Aided Verification of Coordinating Processes-The Automata Theoretic Approach, Princeton University Press, Princeton, NJ (1994)"},{"issue":"1","key":"23_CR13","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1007\/BF01384313","volume":"6","author":"C. Loiseaux","year":"1995","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, Vol. 6(1), (1995) 11\u201344","journal-title":"Formal Methods in System Design"},{"key":"23_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"435","DOI":"10.1007\/10722167_33","volume-title":"Syntactic Program Transformations for Automatic Abstraction","author":"K.S. Namjoshi","year":"2000","unstructured":"K.S. Namjoshi and R P. Kurshan, Syntactic Program Transformations for Automatic Abstraction, In Proc. of CAV\u201900, LNCS 1855, (2000), 435\u2013449"},{"key":"23_CR15","doi-asserted-by":"crossref","unstructured":"Y. Kesten and A. Pnueli, Control and Data Abstraction: Cornerstones of the Practical Formal Verification, Software Tools and Technology Transfer, Vol. 2(4) (2000)","DOI":"10.1007\/s100090050040"},{"key":"23_CR16","unstructured":"SES Inc., ObjectBench Technical Reference, SES Inc. (1998)"},{"key":"23_CR17","unstructured":"N. Sharygina, Model Checking of Software Control Systems, Ph.D. Dissertation, The University of Texas at Austin (2002)"},{"key":"23_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"318","DOI":"10.1007\/3-540-45314-8_23","volume-title":"A Formal Object-Oriented Analysis for Software Reliability: Design for Verification","author":"N. Sharygina","year":"2001","unstructured":"N. Sharygina, J.C. Browne and R. Kurshan, A Formal Object-Oriented Analysis for Software Reliability: Design for Verification, In Proc. of FASE\u201901, LNCS 2029, (2001), 318\u2013332"},{"key":"23_CR19","unstructured":"S. Shlaer, S. Mellor, Object Lifecycles: Modeling the World in States, Pr. Hall (1992)"},{"key":"23_CR20","unstructured":"L. Starr, Executable UML: The Models that Are the Code, M. Integration, LLC (2001)"},{"key":"23_CR21","unstructured":"F. Xie, V. Levin, and J.C. Browne, Model Checking of an Executable Subset of UML, In Proceedings of ASE2001: Automated Software Engineering (2001)"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36578-8_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T22:07:59Z","timestamp":1556921279000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36578-8_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540008996","9783540365785"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-36578-8_23","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}