{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:02:02Z","timestamp":1725487322898},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540404934"},{"type":"electronic","value":"9783540450610"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-45061-0_5","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T11:54:04Z","timestamp":1184586844000},"page":"47-63","source":"Crossref","is-referenced-by-count":6,"title":["Model Checking and Testing Combined"],"prefix":"10.1007","author":[{"given":"Doron","family":"Peled","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,6,18]]},"reference":[{"key":"5_CR1","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0890-5401(87)90052-6","volume":"75","author":"D. Angluin","year":"1978","unstructured":"D. Angluin, Learning Regular Sets from Queries and Counterexamples, Information and Computation, 75, 87\u2013106 (1978).","journal-title":"Information and Computation"},{"key":"5_CR2","unstructured":"J. R. B\u00fcchi. On a decision method in restricted second order arithmetic, Proceedings of the International Congress on Logic, Method and Philosophy in Science 1960, Stanford, CA, 1962. Stanford University Press, 1\u201312."},{"issue":"3","key":"5_CR3","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1109\/TSE.1978.231496","volume":"SE-4","author":"T. S. Chow","year":"1978","unstructured":"T. S. Chow, Testing software design modeled by finite-state machines, IEEE transactions on software engineering, SE-4,3, 1978, 178\u2013187.","journal-title":"IEEE transactions on software engineering"},{"key":"5_CR4","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"E. M. Clarke","year":"2001","unstructured":"E. M. Clarke, A. Biere, R. Raimi, Yunshan Zhu, Bounded Model Checking Using Satisfiability Solving, Formal Methods in System Design 19 (2001), 7\u201334.","journal-title":"Formal Methods in System Design"},{"key":"5_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Workshop on Logic of Programs","author":"E. M. Clarke","year":"1981","unstructured":"E. M. Clarke, E. A. Emerson, Design and synthesis of synchronization skeletons using branching time temporal logic. Workshop on Logic of Programs, Yorktown Heights, NY, Lecture Notes in Computer Science 131, Springer-Verlag, 1981, 52\u201371."},{"key":"5_CR6","unstructured":"E.M. Clarke, O. Grumberg, D. Peled, Model Checking, MIT Press, 2000."},{"key":"5_CR7","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C. Courcoubetis","year":"1992","unstructured":"C. Courcoubetis, M. Y. Vardi, P. Wolper, M. Yannakakis, Memory efficient algorithms for the verification of temporal properties, Formal Methods in System Design, Kluwer, 1 (1992), 275\u2013288.","journal-title":"Formal Methods in System Design"},{"issue":"8","key":"5_CR8","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"E.W. 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":"5_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1007\/3-540-10003-2_69","volume-title":"International Colloquium on Automata, Languages and Programming","author":"E. A. Emerson","year":"1980","unstructured":"E. A. Emerson, E. M. Clarke, Characterizing correctness properties of parallel programs using fixpoints, International Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science 85, Springer-Verlag, July 1980, 169\u2013181."},{"key":"5_CR10","unstructured":"R. Floyd, Assigning meaning to programs, Proceedings of symposium on applied mathematical aspects of computer science, J.T. Schwartz, ed. American Mathematical Society"},{"key":"5_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"431","DOI":"10.1007\/3-540-46002-0_30","volume-title":"Temporal debugging for concurrent systems","author":"E. L. Gunter","year":"2002","unstructured":"E. L. Gunter, D. Peled, Temporal debugging for concurrent systems, TACAS 2002, Grenoble, France, LNCS 2280, Springer, 431\u2013444."},{"key":"5_CR12","series-title":"Lect Notes Comput Sci","volume-title":"Zohar Manna Festschrift","author":"E. L. Gunter","year":"2004","unstructured":"E. L. Gunter, D. Peled, Unit checking: symbolic model checking for a unit of code, in N. Dershovitz (ed.), Zohar Manna Festschrift, LNCS, Springer-Verlag."},{"key":"5_CR13","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\u201318, Chapman & Hall, 1995, 1967, 19\u201332.","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"5_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"357","DOI":"10.1007\/3-540-46002-0_25","volume-title":"Adaptive Model Checking","author":"A. Groce","year":"2002","unstructured":"A. Groce, D. Peled, M. Yannakakis, Adaptive Model Checking, TACAS 2002, LNCS 2280, 357\u2013370."},{"key":"5_CR15","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C. A. R. Hoare","year":"1969","unstructured":"C. A. R. Hoare, An axiomatic basis for computer programming, Communication of the ACM 12 (1969), 576\u2013580.","journal-title":"Communication of the ACM"},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"G. E. Hughes, M. J. Cresswell, A New Introduction to Modal Logic, Routledge, 1996.","DOI":"10.4324\/9780203290644"},{"issue":"7","key":"5_CR17","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"17","author":"J.C. 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"},{"key":"5_CR18","unstructured":"G.J. Myers, The Art of Software Testing, John Wiley and Sons, 1979."},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"R. P. Kurshan. Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, 1994.","DOI":"10.1515\/9781400864041"},{"key":"5_CR20","doi-asserted-by":"publisher","first-page":"1090","DOI":"10.1109\/5.533956","volume":"84","author":"D. Lee","year":"1996","unstructured":"D. Lee, M. Yannakakis, Principles and methods of testing finite state machines \u2014 a survey, Proceedings of the IEEE, 84 (1996), 1090\u20131126.","journal-title":"Proceedings of the IEEE"},{"key":"5_CR21","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":"5_CR22","doi-asserted-by":"crossref","unstructured":"K._L. McMillan, Symbolic Model Checking, Kluwer Academic Press, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"D. Peled, M. Y. Vardi, M. Yannakakis, Black Box Checking, Black Box Checking, FORTE\/PSTV 1999, Beijing, China.","DOI":"10.1007\/978-0-387-35578-8_13"},{"key":"5_CR24","doi-asserted-by":"crossref","unstructured":"A. Pnueli, The temporal logic of programs, 18th IEEE symposium on Foundation of Computer Science, 1977, 46\u201357.","DOI":"10.1109\/SFCS.1977.32"},{"key":"5_CR25","doi-asserted-by":"crossref","unstructured":"J. P. Quielle, J. Sifakis, Specification and verification of concurrent systems in CESAR, Proceedings of the 5th International Symposium on Programming, 1981, 337\u2013350.","DOI":"10.1007\/3-540-11494-7_22"},{"issue":"4","key":"5_CR26","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1109\/TSE.1985.232226","volume":"SE-11","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-114(1985), 367\u2013375.","journal-title":"IEEE Transactions on software engineering"},{"key":"5_CR27","first-page":"133","volume-title":"Handbook of Theoretical Computer Science","author":"W. Thomas","year":"1990","unstructured":"W. Thomas, Automata on infinite objects, In Handbook of Theoretical Computer Science, vol. B, J. van Leeuwen, ed., Elsevier, Amsterdam (1990) 133\u2013191."},{"key":"5_CR28","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"R. E. Tarjan","year":"1972","unstructured":"R. E. Tarjan, Depth first search and linear graph algorithms, SIAM Journal of computing, 1 (1972).,146\u2013160.","journal-title":"SIAM Journal of computing"},{"key":"5_CR29","unstructured":"M. Y. Vardi, P. Wolper, An automata-theoretic approach to automatic program verification, Proceedings of the 1st Annual Symposium on Logic in Computer Science IEEE, 1986, 332\u2013344."},{"key":"5_CR30","unstructured":"M. P. Vasilevskii, Failure diagnosis of automata, Kibertetika"}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45061-0_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,30]],"date-time":"2019-04-30T23:15:10Z","timestamp":1556666110000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45061-0_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540404934","9783540450610"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/3-540-45061-0_5","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}