[{"abstract":[{"text":"We have extended the software model checker BLAST to automatically generate test suites that guarantee full coverage with respect to a given predicate. More precisely, given a C program and a target predicate p, BLAST determines the set L of program locations which program execution can reach with p true, and automatically generates a set of test vectors that exhibit the truth of p at all locations in L. We have used BLAST to generate test suites and to detect dead code in C programs with up to 30 K lines of code. The analysis and test vector generation is fully automatic (no user intervention) and exact (no false positives).","lang":"eng"}],"extern":"1","publication_status":"published","type":"conference","oa_version":"None","quality_controlled":"1","year":"2004","date_created":"2018-12-11T12:09:35Z","author":[{"full_name":"Beyer, Dirk","last_name":"Beyer","first_name":"Dirk"},{"full_name":"Chlipala, Adam","last_name":"Chlipala","first_name":"Adam"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"},{"last_name":"Jhala","first_name":"Ranjit","full_name":"Jhala, Ranjit"},{"last_name":"Majumdar","first_name":"Ritankar","full_name":"Majumdar, Ritankar"}],"status":"public","title":"Generating tests from counterexamples","_id":"4581","date_updated":"2026-05-29T07:46:59Z","fulldoi":"https://doi.org/10.1109/ICSE.2004.1317455","user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","article_processing_charge":"No","citation":{"chicago":"Beyer, Dirk, Adam Chlipala, Thomas A Henzinger, Ranjit Jhala, and Ritankar Majumdar. “Generating Tests from Counterexamples.” In <i>Proceedings of the 26th International Conference on Software Engineering</i>, 326–35. IEEE, 2004. <a href=\"https://doi.org/10.1109/ICSE.2004.1317455\">https://doi.org/10.1109/ICSE.2004.1317455</a>.","apa":"Beyer, D., Chlipala, A., Henzinger, T. A., Jhala, R., &#38; Majumdar, R. (2004). Generating tests from counterexamples. In <i>Proceedings of the 26th International Conference on Software Engineering</i> (pp. 326–335). Edinburgh, United Kingdom: IEEE. <a href=\"https://doi.org/10.1109/ICSE.2004.1317455\">https://doi.org/10.1109/ICSE.2004.1317455</a>","ama":"Beyer D, Chlipala A, Henzinger TA, Jhala R, Majumdar R. Generating tests from counterexamples. In: <i>Proceedings of the 26th International Conference on Software Engineering</i>. IEEE; 2004:326-335. doi:<a href=\"https://doi.org/10.1109/ICSE.2004.1317455\">10.1109/ICSE.2004.1317455</a>","mla":"Beyer, Dirk, et al. “Generating Tests from Counterexamples.” <i>Proceedings of the 26th International Conference on Software Engineering</i>, IEEE, 2004, pp. 326–35, doi:<a href=\"https://doi.org/10.1109/ICSE.2004.1317455\">10.1109/ICSE.2004.1317455</a>.","ieee":"D. Beyer, A. Chlipala, T. A. Henzinger, R. Jhala, and R. Majumdar, “Generating tests from counterexamples,” in <i>Proceedings of the 26th International Conference on Software Engineering</i>, Edinburgh, United Kingdom, 2004, pp. 326–335.","short":"D. Beyer, A. Chlipala, T.A. Henzinger, R. Jhala, R. Majumdar, in:, Proceedings of the 26th International Conference on Software Engineering, IEEE, 2004, pp. 326–335.","ista":"Beyer D, Chlipala A, Henzinger TA, Jhala R, Majumdar R. 2004. Generating tests from counterexamples. Proceedings of the 26th International Conference on Software Engineering. ICSE: Software Engineering, 326–335."},"page":"326 - 335","conference":{"location":"Edinburgh, United Kingdom","end_date":"2004-05-28","start_date":"2004-05-23","name":"ICSE: Software Engineering"},"date_published":"2004-07-26T00:00:00Z","publisher":"IEEE","month":"07","publication_identifier":{"isbn":["0769521630"],"issn":["0270-5257"]},"scopus_import":"1","day":"26","publication":"Proceedings of the 26th International Conference on Software Engineering","doi":"10.1109/ICSE.2004.1317455","publist_id":"128","language":[{"iso":"eng"}],"OA_type":"closed access"}]