{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,20]],"date-time":"2026-05-20T20:42:34Z","timestamp":1779309754054,"version":"3.51.4"},"reference-count":47,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2014,5,31]],"date-time":"2014-05-31T00:00:00Z","timestamp":1401494400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Software Qual J"],"published-print":{"date-parts":[[2015,3]]},"DOI":"10.1007\/s11219-014-9237-3","type":"journal-article","created":{"date-parts":[[2014,5,30]],"date-time":"2014-05-30T09:03:35Z","timestamp":1401440615000},"page":"171-202","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["PBCOV: a property-based coverage criterion"],"prefix":"10.1007","volume":"23","author":[{"given":"Kassem","family":"Fawaz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fadi","family":"Zaraket","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wes","family":"Masri","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hamza","family":"Harkous","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,5,31]]},"reference":[{"key":"9237_CR1","unstructured":"ABC. (2007). ABC: Berkeley logic synthesis and verification group. a system for sequential synthesis and verification, release 70930. http:\/\/www.eecs.berkeley.edu\/alanmi\/abc\/ ."},{"key":"9237_CR2","doi-asserted-by":"crossref","unstructured":"Ammann, P., & Black, P. E. (2001). A specification-based coverage metric to evaluate test sets. International Journal of Reliability, Quality and Safety Engineering, 8(4), 239\u2013248.","DOI":"10.1142\/S0218539301000530"},{"key":"9237_CR3","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511809163","volume-title":"Introduction to software testing","author":"P Ammann","year":"2008","unstructured":"Ammann, P., & Offutt, J. (2008). Introduction to software testing (1st ed.). New York, NY: Cambridge University Press.","edition":"1"},{"key":"9237_CR4","unstructured":"Ball, T. (2004). A theory of predicate-complete test coverage and generation. In In FMCO 2004: Symposium on formal methods for components and objects, pp 1\u201322."},{"key":"9237_CR5","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T., & Rajamani, SK. (2001). Automatic predicate abstraction of c programs. In Programming language design and implementation, ACM, New York, NY, USA, PLDI \u201901, pp. 203\u2013213.","DOI":"10.1145\/378795.378846"},{"key":"9237_CR6","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1145\/1965724.1965743","volume":"54","author":"T Ball","year":"2011","unstructured":"Ball, T., Levin, V., & Rajamani, S. K. (2011). A decade of software model checking with slam. Communications of the ACM, 54, 68\u201376.","journal-title":"Communications of the ACM"},{"key":"9237_CR7","volume-title":"Find the bug: A iook of incorrect programs","author":"A Barr","year":"2004","unstructured":"Barr, A. (2004). Find the bug: A iook of incorrect programs. Reading: Addison-Wesley Professional."},{"key":"9237_CR8","unstructured":"Baudin, P., Filli\u00e2tre, J.C., Hubert, T., March\u00e9, C., Monate, B., Moy, Y., et al. (2009). ACSL: ANSI C specification language (preliminary design V1.9). http:\/\/www.frama-c.cea.fr\/acsl.html ."},{"key":"9237_CR9","doi-asserted-by":"crossref","unstructured":"Boyapati, C., Khurshid, S., & Marinov, D. (2002). Korat: Automated testing based on java predicates. In International symposium on software testing and analysis (ISSTA), pp. 123\u2013133.","DOI":"10.1145\/566172.566191"},{"key":"9237_CR10","doi-asserted-by":"crossref","unstructured":"Burnim, J., & Sen, K. (2008). Heuristics for scalable dynamic test generation. In International conference on automated software engineering, pp. 443\u2013446.","DOI":"10.1109\/ASE.2008.69"},{"key":"9237_CR11","doi-asserted-by":"crossref","unstructured":"Chang, J., & Richardson, DJ. (1999). Structural specification-based testing: Automated support and experimental evaluation. In European, software engineering conference, ESEC\/FSE-7, pp. 285\u2013302.","DOI":"10.1007\/3-540-48166-4_18"},{"key":"9237_CR12","volume-title":"Model checking","author":"E Clarke","year":"1999","unstructured":"Clarke, E., Brumberg, J. O., & Peled, D. A. (1999). Model checking. Cambridge: MIT Press."},{"key":"9237_CR13","doi-asserted-by":"crossref","unstructured":"Clarke, E., Kroening, D., & Lerda, F. (2004). A tool for checking ansi-c programs. In Tools and algorithms for the construction and analysis of systems, pp. 168\u2013176.","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"9237_CR14","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1145\/503271.503230","volume":"26","author":"A Coen-Porisini","year":"2001","unstructured":"Coen-Porisini, A., Denaro, G., Ghezzi, C., & Pezz\u00e9, M. (2001). Using symbolic execution for verifying safety-critical systems. ACM SIGSOFT Software Engineering Notes, 26, 142\u2013151.","journal-title":"ACM SIGSOFT Software Engineering Notes"},{"key":"9237_CR15","volume-title":"Introduction to algorithms","author":"TH Cormen","year":"2009","unstructured":"Cormen, T. H., Stein, C., Rivest, R. L., & Leiserson, C. E. (2009). Introduction to algorithms (3rd ed.). Cambridge: MIT Press.","edition":"3"},{"key":"9237_CR16","doi-asserted-by":"crossref","first-page":"34","DOI":"10.1109\/C-M.1978.218136","volume":"11","author":"RA DeMillo","year":"1978","unstructured":"DeMillo, R. A., Lipton, R. J., & Sayward, F. G. (1978). Hints on test data selection: Help for the practicing programmer. Computer, 11, 34\u201341.","journal-title":"Computer"},{"key":"9237_CR17","doi-asserted-by":"crossref","first-page":"405","DOI":"10.1007\/s10664-005-3861-2","volume":"10","author":"H Do","year":"2005","unstructured":"Do, H., Elbaum, S., & Rothermel, G. (2005). Supporting controlled experimentation with testing techniques: An infrastructure and its potential impact. Empirical Software Engineering, 10, 405\u2013435.","journal-title":"Empirical Software Engineering"},{"key":"9237_CR18","doi-asserted-by":"crossref","unstructured":"Dutertre, B., & Moura, L. M. D. (2006). A fast linear-arithmetic solver for dpll(t). Computer Aided Verification.","DOI":"10.1007\/11817963_11"},{"key":"9237_CR19","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1016\/j.scico.2007.01.015","volume":"69","author":"MD Ernst","year":"2007","unstructured":"Ernst, M. D., Perkins, J. H., Guo, P. J., McCamant, S., Pacheco, C., Tschantz, M. S., & Xiao, C. (2007). The daikon system for dynamic detection of likely invariants. Science of Computer Programming, 69, 35\u201345.","journal-title":"Science of Computer Programming"},{"key":"9237_CR20","doi-asserted-by":"crossref","unstructured":"Ford, L. R., & Fulkerson, D. R. (1956). Maximal flow through a network. Canadian Journal of Mathematics, 8, 399\u2013404.","DOI":"10.4153\/CJM-1956-045-5"},{"key":"9237_CR21","doi-asserted-by":"crossref","unstructured":"Gligoric, M., Gvero, T., Jagannath, V., Khurshid, S., Kuncak, V., & Marinov, D. (2010). Test generation through programming in udita. In International conference on software engineering, ACM, ICSE \u201910.","DOI":"10.1145\/1806799.1806835"},{"key":"9237_CR22","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Klarlund, N., & Sen, K. (2005). Dart: Directed automated random testing. In Proceedings of the 2005 ACM SIGPLAN conference on programming language design and implementation, ACM, PLDI \u201905.","DOI":"10.1145\/1065010.1065036"},{"key":"9237_CR23","unstructured":"Gough, B. J., & Stallman, R. M. (2005). An introduction to GCC. Network Theory Ltd"},{"key":"9237_CR24","doi-asserted-by":"crossref","unstructured":"Harder, M., Mellen, J., & Ernst, M. D. (2003). Improving test suites via operational abstraction. In International conference on software engineering, pp. 60\u201371.","DOI":"10.1109\/ICSE.2003.1201188"},{"key":"9237_CR25","unstructured":"Heimdahl, M. P. E., Rayadurgam, S., Visser, W., Devaraj, G., & Gao, J. (2003). Auto-generating test sequences using model checkers: A case study. In Workshop on formal approaches to testing of software, pp 42\u201359."},{"key":"9237_CR26","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann, G. J. (1997). The model checker spin. IEEE Transactions on Software Engineering, 23, 279\u2013295.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"9237_CR27","doi-asserted-by":"crossref","unstructured":"Horgan, J. R., & London, S. (1991). Data flow coverage and the c language. In Proceedings of the symposium on testing, analysis, and verification, TAV4, pp. 87\u201397.","DOI":"10.1145\/120807.120815"},{"key":"9237_CR28","doi-asserted-by":"crossref","unstructured":"Jaygarl, H., Lu, K. S., & Chang, C. K. (2010). Genred: A tool for generating and reducing object-oriented test cases. In IEEE annual computer software and applications conference, pp. 127\u2013136.","DOI":"10.1109\/COMPSAC.2010.19"},{"key":"9237_CR29","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1023\/B:AUSE.0000038938.10589.b9","volume":"11","author":"S Khurshid","year":"2004","unstructured":"Khurshid, S., & Marinov, D. (2004). Testera: Specification-based testing of java programs using sat. Automated Software Engineering, 11, 403\u2013434.","journal-title":"Automated Software Engineering"},{"key":"9237_CR30","volume-title":"An introduction to formal languages and automata","author":"P Linz","year":"2012","unstructured":"Linz, P. (2012). An introduction to formal languages and automata (5th ed.). Burlington: Jones and Bartlett Learning.","edition":"5"},{"key":"9237_CR31","unstructured":"Martinian, E. (2010). Red-black tree c code. http:\/\/www.mit.edu\/emin\/source_code\/red_black_tree ."},{"key":"9237_CR32","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1002\/stvr.409","volume":"20","author":"W Masri","year":"2010","unstructured":"Masri, W. (2010). Fault localization based on information flow coverage. Software Testing, Verification and Reliability, 20, 121\u2013147.","journal-title":"Software Testing, Verification and Reliability"},{"key":"9237_CR33","doi-asserted-by":"crossref","unstructured":"Masri, W., & Abou-Assi, R. (2010). Cleansing test suites from coincidental correctness to enhance fault-localization. In International conference on software testing, verification and validation, ICST \u201910.","DOI":"10.1109\/ICST.2010.22"},{"key":"9237_CR34","doi-asserted-by":"crossref","first-page":"454","DOI":"10.1109\/TSE.2007.1020","volume":"33","author":"W Masri","year":"2007","unstructured":"Masri, W., Podgurski, A., & Leon, D. (2007). An empirical study of test case filtering techniques based on exercising information flows. IEEE Transactions on Software Engineering, 33, 454\u2013477.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"9237_CR35","unstructured":"McMillan, K. L. (1998). The smv language: Cadence berkeley labs. Technical report."},{"key":"9237_CR36","doi-asserted-by":"crossref","unstructured":"Necula, G. C., Mcpeak, S., Rahul, S. P., & Weimer, W. (2002). Cil: Intermediate language and tools for analysis and transformation of c programs. In International conference on compiler, construction, pp. 213\u2013228.","DOI":"10.1007\/3-540-45937-5_16"},{"key":"9237_CR37","unstructured":"PBCOV-APPENDICES. (2013). PBCOV-APPENDICES. http:\/\/webfea.fea.aub.edu.lb\/fadi\/dkwk\/doku.php?id=pbcov ."},{"key":"9237_CR38","unstructured":"PBCOV-TOOL. (2013). PBCOV-TOOL. http:\/\/webfea.fea.aub.edu.lb\/fadi\/dkwk\/doku.php?id=pbcov ."},{"key":"9237_CR39","unstructured":"Rapps, S., & Weyuker, E. J. (1982). Data flow analysis techniques for test data selection. In International conference on Software engineering (pp. 272\u2013278). CA, USA: Los Alamitos."},{"key":"9237_CR40","doi-asserted-by":"crossref","unstructured":"Santelices, R. A., Chittimalli, P. K., Apiwattanapong, T., Orso, A., & Harrold, M. J. (2008). Test-suite augmentation for evolving software. In ASE, pp 218\u2013227.","DOI":"10.1109\/ASE.2008.32"},{"key":"9237_CR41","doi-asserted-by":"crossref","unstructured":"Schuler, D., & Zeller, A. (2011). Assessing oracle quality with checked coverage. In International conference on software testing, verification and validation, pp. 90\u201399.","DOI":"10.1109\/ICST.2011.32"},{"key":"9237_CR42","doi-asserted-by":"crossref","unstructured":"Torlak, E., & Jackson, D. (2007). Kodkod: A relational model finder. In Proceedings of the 13th international conference on tools and algorithms for the construction and analysis of systems, TACAS\u201907.","DOI":"10.1007\/978-3-540-71209-1_49"},{"issue":"2","key":"9237_CR43","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1023\/A:1022920129859","volume":"10","author":"W Visser","year":"2003","unstructured":"Visser, W., Havelund, K., Brat, G. P., Park, S., & Lerda, F. (2003). Model checking programs. Automated Software Engineering Journal, 10(2), 203\u2013232.","journal-title":"Automated Software Engineering Journal"},{"key":"9237_CR44","doi-asserted-by":"crossref","first-page":"19:1","DOI":"10.1145\/1592434.1592436","volume":"41","author":"J Woodcock","year":"2009","unstructured":"Woodcock, J., Larsen, P. G., Bicarregui, J., & Fitzgerald, J. (2009). Formal methods: Practice and experience. ACM Computing Surveys, 41, 19:1\u201319:36.","journal-title":"ACM Computing Surveys"},{"key":"9237_CR45","doi-asserted-by":"crossref","unstructured":"Yang, J., & Evans, D. (2004). Dynamically inferring temporal properties. In SIGPLAN-SIGSOFT workshop on program analysis for software tools and engineering, PASTE \u201904, pp 23\u201328.","DOI":"10.1145\/996821.996832"},{"issue":"1","key":"9237_CR46","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1093\/comjnl\/bxn075","volume":"53","author":"X Yang","year":"2010","unstructured":"Yang, X., Wang, J., & Yi, X. (2010). Slicing execution with partial weakest precondition for model abstraction of c programs. The Computer Journal, 53(1), 37\u201349.","journal-title":"The Computer Journal"},{"key":"9237_CR47","doi-asserted-by":"crossref","unstructured":"Zaraket, F., & Masri, W. (2009). Property based coverage criterion. In International workshop on defects in large software systems, DEFECTS \u201909, pp. 27\u201328.","DOI":"10.1145\/1555860.1555870"}],"container-title":["Software Quality Journal"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11219-014-9237-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11219-014-9237-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11219-014-9237-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,11]],"date-time":"2019-08-11T04:13:00Z","timestamp":1565496780000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11219-014-9237-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,5,31]]},"references-count":47,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,3]]}},"alternative-id":["9237"],"URL":"https:\/\/doi.org\/10.1007\/s11219-014-9237-3","relation":{},"ISSN":["0963-9314","1573-1367"],"issn-type":[{"value":"0963-9314","type":"print"},{"value":"1573-1367","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,5,31]]}}}