{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T21:55:08Z","timestamp":1770328508838,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540291312","type":"print"},{"value":"9783540319399","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11561163_1","type":"book-chapter","created":{"date-parts":[[2005,9,27]],"date-time":"2005-09-27T14:54:31Z","timestamp":1127832871000},"page":"1-22","source":"Crossref","is-referenced-by-count":47,"title":["A Theory of Predicate-Complete Test Coverage and Generation"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Ball","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"6","key":"1_CR1","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1145\/390016.808445","volume":"10","author":"R. Boyer","year":"1975","unstructured":"Boyer, R., Elspas, B., Levitt, K.: SELECT\u2013a formal system for testing and debugging programs by symbolic execution. SIGPLAN Notices\u00a010(6), 234\u2013245 (1975)","journal-title":"SIGPLAN Notices"},{"key":"1_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/3-540-48683-6_25","volume-title":"Computer Aided Verification","author":"G. Bruns","year":"1999","unstructured":"Bruns, G., Godefroid, P.: Model checking partial state spaces with 3-valued temporal logics. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 274\u2013287. Springer, Heidelberg (1999)"},{"key":"1_CR3","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1145\/566172.566191","volume-title":"Proceedings of the International Symposium on Software Testing and Analysis","author":"C. Boyapati","year":"2002","unstructured":"Boyapati, C., Khurshid, S., Marinov, D.: Korat: automated testing based on java predicates. In: Proceedings of the International Symposium on Software Testing and Analysis, pp. 123\u2013133. ACM, New York (2002)"},{"issue":"7","key":"1_CR4","doi-asserted-by":"publisher","first-page":"775","DOI":"10.1002\/(SICI)1097-024X(200006)30:7<775::AID-SPE309>3.0.CO;2-H","volume":"30","author":"W.R. Bush","year":"2000","unstructured":"Bush, W.R., Pincus, J.D., Sielaff, D.J.: A static analyzer for finding dynamic programming errors. Software-Practice and Experience\u00a030(7), 775\u2013802 (2000)","journal-title":"Software-Practice and Experience"},{"key":"1_CR5","volume-title":"ICSE 2004: International Conference on Software Engineering","author":"A.J. Chlipala","year":"2004","unstructured":"Chlipala, A.J., Henzinger, T.A., Jhala, R., Majumdar, R.: Generating tests from counterexamples. In: ICSE 2004: International Conference on Software Engineering. ACM, New York (2004) (to appear)"},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Clarke, E., Kroening, D., Yorav, K.: Behavioral consistency of C and Verilog programs using bounded model checking. In: Design Automation Conference, pp. 368\u2013371 (2003)","DOI":"10.21236\/ADA461052"},{"issue":"3","key":"1_CR7","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1109\/TSE.1976.233817","volume":"2","author":"L.A. Clarke","year":"1976","unstructured":"Clarke, L.A.: A system to generate test data and symbolically execute programs. IEEE Transactions on Software Engineering\u00a02(3), 215\u2013222 (1976)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"1_CR8","series-title":"Lecture Notes in Computer Science","volume-title":"LICS 2004: Logic in Computer Science","author":"L. Alfaro de","year":"2004","unstructured":"de Alfaro, L., Godefroid, P., Jagadeesan, R.: Three-valued abstractions of games: uncertainty, but with precision. In: LICS 2004: Logic in Computer Science. LNCS. Springer, Heidelberg (2004) (to appear)"},{"key":"1_CR9","first-page":"53","volume-title":"Proceedings of the International Symposium on Software Testing and Analysis","author":"A. Gotlieb","year":"1998","unstructured":"Gotlieb, A., Botella, B., Rueher, M.: Automatic test data generation using constraint solving techniques. In: Proceedings of the International Symposium on Software Testing and Analysis, pp. 53\u201362. ACM, New York (1998)"},{"key":"1_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"426","DOI":"10.1007\/3-540-44685-0_29","volume-title":"CONCUR 2001 - Concurrency Theory","author":"P. Godefroid","year":"2001","unstructured":"Godefroid, P., Huth, M., Jagadeesan, R.: Abstraction-based model checking using modal transition systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol.\u00a02154, pp. 426\u2013440. Springer, Heidelberg (2001)"},{"key":"1_CR11","volume-title":"FSE 1998: Foundations of Software Engineering","author":"N. Gupta","year":"1998","unstructured":"Gupta, N., Mathur, A.P., Soffa, M.L.: Automated test data generation using an iterative relaxation method. In: FSE 1998: Foundations of Software Engineering. ACM, New York (1998)"},{"key":"1_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-540-45212-6_15","volume-title":"Embedded Software","author":"P. Godefroid","year":"2003","unstructured":"Godefroid, P.: Reasoning about abstract open systems with generalized module checking. In: Alur, R., Lee, I. (eds.) EMSOFT 2003. LNCS, vol.\u00a02855, pp. 223\u2013240. Springer, Heidelberg (2003)"},{"key":"1_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/3-540-36384-X_18","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P. Godefroid","year":"2002","unstructured":"Godefroid, P., Jagadeesan, R.: On the expressiveness of 3-valued models. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol.\u00a02575, pp. 206\u2013222. Springer, Heidelberg (2002)"},{"key":"1_CR14","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-5983-1","volume-title":"The Science of Programming","author":"D. Gries","year":"1981","unstructured":"Gries, D.: The Science of Programming. Springer, Heidelberg (1981)"},{"issue":"2","key":"1_CR15","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1145\/333979.333989","volume":"47","author":"R. Giacobazzi","year":"2000","unstructured":"Giacobazzi, R., Ranzato, F., Scozzari, F.: Making abstract interpretations complete. Journal of the ACM\u00a047(2), 361\u2013416 (2000)","journal-title":"Journal of the ACM"},{"key":"1_CR16","doi-asserted-by":"crossref","first-page":"60","DOI":"10.1109\/ICSE.2003.1201188","volume-title":"ICSE 2003: International Conference on Software Engineering","author":"M. Harder","year":"2003","unstructured":"Harder, M., Mellen, J., Ernst, M.D.: Improving test suites via operational abstraction. In: ICSE 2003: International Conference on Software Engineering, pp. 60\u201371. ACM, New York (2003)"},{"key":"1_CR17","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1109\/TSE.1976.233816","volume":"2","author":"W.E. Howden","year":"1976","unstructured":"Howden, W.E.: Reliability of the path analysis testing strategy. IEEE Transactions on Software Engineering\u00a02, 208\u2013215 (1976)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"1_CR18","first-page":"95","volume-title":"Proceedings of the International Symposium on Software Testing and Analysis","author":"R. Jasper","year":"1994","unstructured":"Jasper, R., Brennan, M., Williamson, K., Currier, B., Zimmerman, D.: Test data generation and feasible path analysis. In: Proceedings of the International Symposium on Software Testing and Analysis, pp. 95\u2013107. ACM, New York (1994)"},{"key":"1_CR19","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1145\/347324.383378","volume-title":"Proceedings of the International Symposium on Software Testing and Analysis","author":"D. Jackson","year":"2000","unstructured":"Jackson, D., Vaziri, M.: Finding bugs with a constraint solver. In: Proceedings of the International Symposium on Software Testing and Analysis, pp. 14\u201325. ACM, New York (2000)"},{"issue":"4","key":"1_CR20","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1002\/stvr.4370020405","volume":"2","author":"B. Korel","year":"1992","unstructured":"Korel, B.: Dynamic method of software test data generation. Software Testing, Verification and Reliability\u00a02(4), 203\u2013213 (1992)","journal-title":"Software Testing, Verification and Reliability"},{"key":"1_CR21","volume-title":"Communicating and Mobile Systems: the \u03c0-Calculus","author":"R. Milner","year":"1999","unstructured":"Milner, R.: Communicating and Mobile Systems: the \u03c0-Calculus. Cambridge University Press, Cambridge (1999)"},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"Ramamoorthy, C., Ho, S., Chen, W.: On the automated generation of program test data. IEEE Transactions on Software Engineering\u00a02(4), 293\u2013300","DOI":"10.1109\/TSE.1976.233835"},{"key":"1_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"546","DOI":"10.1007\/978-3-540-24730-2_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Shoham","year":"2004","unstructured":"Shoham, S., Grumberg, O.: Monotonic abstraction-refinement for CTL. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 546\u2013560. Springer, Heidelberg (2004)"},{"issue":"8","key":"1_CR24","doi-asserted-by":"publisher","first-page":"552","DOI":"10.1109\/32.536956","volume":"22","author":"K.-C. Tai","year":"1996","unstructured":"Tai, K.-C.: Theory of fault-based predicate testing for computer programs. IEEE Transactions on Software Engineering\u00a022(8), 552\u2013562 (1996)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"1_CR25","doi-asserted-by":"crossref","unstructured":"Tai, K.-C.: Predicate-based test generation for computer programs. In: ICSE 1997: International Conference on Software Engineering, pp. 267\u2013276 (1997)","DOI":"10.1109\/ICSE.1993.346037"},{"key":"1_CR26","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1145\/75308.75315","volume-title":"Proceedings of the Symposium on Software Testing, Analysis, and Verification","author":"D. Yates","year":"1989","unstructured":"Yates, D., Malevris, N.: Reducing the effects of infeasible paths in branch testing. In: Proceedings of the Symposium on Software Testing, Analysis, and Verification, pp. 48\u201354. ACM, New York (1989)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Components and Objects"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11561163_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,4]],"date-time":"2025-01-04T16:02:14Z","timestamp":1736006534000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11561163_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540291312","9783540319399"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/11561163_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}