{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,7]],"date-time":"2026-01-07T07:59:56Z","timestamp":1767772796518},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540210023"},{"type":"electronic","value":"9783540399100"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-39910-0_24","type":"book-chapter","created":{"date-parts":[[2014,3,18]],"date-time":"2014-03-18T06:40:04Z","timestamp":1395124804000},"page":"548-567","source":"Crossref","is-referenced-by-count":4,"title":["Unit Checking: Symbolic Model Checking for a Unit of Code"],"prefix":"10.1007","author":[{"given":"Elsa","family":"Gunter","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Doron","family":"Peled","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"24_CR1","doi-asserted-by":"crossref","unstructured":"T. Bultan, R. Gerber, W. Pugh, Model-Checking Concurrent Systems with Unbounded Integer Variables: Symbolic Representation, and Experimental Results, ACM Transactions on Programming and Systems, 21, 1999, 747-789.","DOI":"10.1145\/325478.325480"},{"key":"24_CR2","unstructured":"E.M. Clarke, O. Grumberg, D. Peled, Model Checking, MIT Press, 2000."},{"issue":"8","key":"24_CR3","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"EW Dijkstra","year":"1975","unstructured":"E.W. Dijkstra, Guarded Commands, Nondeterminacy and Formal Derivation of Programs, Communication of the ACM 18(8), 1975, 453\u2013457.","journal-title":"Communication of the ACM"},{"key":"24_CR4","doi-asserted-by":"crossref","unstructured":"C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J.B. Saxe, R. Stata, Extended Static Checking for Java, PLDI 2002, 234-245.","DOI":"10.1145\/543552.512558"},{"key":"24_CR5","doi-asserted-by":"publisher","first-page":"1203","DOI":"10.1002\/1097-024X(200009)30:11<1203::AID-SPE338>3.0.CO;2-N","volume":"30","author":"ER Gansner","year":"2000","unstructured":"E.R. Gansner, S.C. North, An open graph visualization system and its applications to software engineering, Software \u2014 Practice and Experience, 30(2000), 1203\u20131233.","journal-title":"Software \u2014 Practice and Experience"},{"key":"24_CR6","doi-asserted-by":"crossref","unstructured":"E.L. Gunter, D. Peled, Temporal Debugging for Concurrent Systems, TACAS 2002, Grenoble, France, LNCS 2280, Springer, 431-444.","DOI":"10.1007\/3-540-46002-0_30"},{"key":"24_CR7","doi-asserted-by":"crossref","unstructured":"R. Gerth, D. Peled, M.Y. Vardi, P. Wolper, Simple On-the-fly Automatic Verification of Linear Temporal Logic, PSTV95, Protocol Specification Testing and Verification, 3-18, Chapman & Hall, 1995","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"24_CR8","unstructured":"M.J.C. Gordon, T. Melham, Introduction to HOL, Cambridge University Press."},{"key":"24_CR9","doi-asserted-by":"crossref","unstructured":"H.S. Hong, I. Lee, O. Sokolsky, H. Ural, A temporal Logic Based Theory of Test Coverage and Generation, Tools and Algorithms for the Construction and Analysis of Systems, 327-341.","DOI":"10.1007\/3-540-46002-0_23"},{"key":"24_CR10","doi-asserted-by":"crossref","unstructured":"Y. Kesten, A. Pnueli, M.Y. Vardi, Verification by Augmented Abstraction: The Automata-Theoretic View, JCSS 62, 2001, 668-690.","DOI":"10.1006\/jcss.2000.1744"},{"key":"24_CR11","doi-asserted-by":"crossref","unstructured":"M. Kaufmann, P. Manolios, J.S. Moore, Computer-Aided Reasoning: An Approach, Kluwer 2000.","DOI":"10.1007\/978-1-4615-4449-4"},{"issue":"7","key":"24_CR12","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"17","author":"JC King","year":"1976","unstructured":"J.C. King, Symbolic Execution and Program Testing, Communication of the ACM, 17(7), 1976, 385\u2013395.","journal-title":"Communication of the ACM"},{"issue":"2","key":"24_CR13","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1017\/S0956796899003421","volume":"9","author":"C L\u00fcth","year":"1999","unstructured":"C. L\u00fcth, B. Wolff Functional Design and Implementation of Graphical User Interfaces for Theorem Provers, Journal of Functional Programming, 9(2):167\u2013189, March 1999.","journal-title":"Journal of Functional Programming"},{"key":"24_CR14","unstructured":"Y. Matiyasevich, Hilbert\u2019s Tenth Problem, MIT Press, 1993."},{"key":"24_CR15","unstructured":"G.J. Myers, The Art of Software Testing, John Wiley and Sons, 1979."},{"key":"24_CR16","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/0304-3975(91)90041-Y","volume":"83","author":"Z Manna","year":"1991","unstructured":"Z. Manna, A. Pnueli, Completing the Temporal Picture, Theoretical Computer Science 83, 1991, 97\u2013130.","journal-title":"Theoretical Computer Science"},{"key":"24_CR17","doi-asserted-by":"crossref","unstructured":"Z. Manna, A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems: Specification, Springer-Verlag, 1991.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"24_CR18","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2319.001.0001","volume-title":"The Definition of Standard ML (Revised)","author":"R Milner","year":"1997","unstructured":"Robin Milner, Mads Tofte, Robert Harper, and David MacQueen The Definition of Standard ML (Revised). MIT Press, Cambridge, MA, 1997."},{"issue":"3","key":"24_CR19","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1016\/0022-0000(78)90021-1","volume":"16","author":"DC Oppen","year":"1978","unstructured":"D. C. Oppen, A <m:math display=\"block\"> <m:mrow> <m:msup> <m:mn>2<\/m:mn> <m:mrow> <m:msup> <m:mn>2<\/m:mn> <m:mrow> <m:msup> <m:mn>2<\/m:mn> <m:mrow> <m:mi>p<\/m:mi><m:mi>n<\/m:mi> <\/m:mrow> <\/m:msup> <\/m:mrow> <\/m:msup> <\/m:mrow> <\/m:msup> <\/m:mrow> <\/m:math> $$2^{2^{2^{pn} } }$$ upper bound on the complexity of Presburger arithmetic. JCSS 16(3):323\u2013332 (1978).","journal-title":"JCSS"},{"key":"24_CR20","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1109\/TSE.1985.232226","volume":"4","author":"S Rapps","year":"1985","unstructured":"S. Rapps, E. J. Weyuker, Selecting software test data using data flow information, IEEE Transactions on software engineering, SE-11 4(1985), 367\u2013375.","journal-title":"IEEE Transactions on software engineering, SE-11"},{"issue":"9","key":"24_CR21","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1109\/32.713327","volume":"24","author":"JM Rushby","year":"1998","unstructured":"J.M. Rushby, S. Owre, N. Shankar, Subtypes for Specifications: Predicate Subtyping in PVS, Transactions on Software Engineering, 24(9), 1998, 709\u2013720.","journal-title":"Transactions on Software Engineering"},{"key":"24_CR22","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1109\/71.342135","volume":"6","author":"W Pugh","year":"1995","unstructured":"W. Pugh, D. Wonnacott, Going Beyond Integer Programming with the Omega Test to Eliminate False Data Dependencies, IEEE Transactions on Parallel and Distributed Systems 6, 1995, 204\u2013211.","journal-title":"IEEE Transactions on Parallel and Distributed Systems"},{"key":"24_CR23","doi-asserted-by":"crossref","unstructured":"S. Visvanathan, N. Gupta, Generating Test Data for Functions with Point Input, 17th IEEE International Conference on Automated Software Engineering, 2002.","DOI":"10.1109\/ASE.2002.1115007"}],"container-title":["Lecture Notes in Computer Science","Verification: Theory and Practice"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-39910-0_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,25]],"date-time":"2024-05-25T02:23:33Z","timestamp":1716603813000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-39910-0_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540210023","9783540399100"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-39910-0_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}