{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,7]],"date-time":"2026-01-07T07:52:50Z","timestamp":1767772370144,"version":"build-2065373602"},"reference-count":24,"publisher":"Association for Computing Machinery (ACM)","issue":"11","license":[{"start":{"date-parts":[[2022,10,20]],"date-time":"2022-10-20T00:00:00Z","timestamp":1666224000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Commun. ACM"],"published-print":{"date-parts":[[2022,11]]},"DOI":"10.1145\/3551665","type":"journal-article","created":{"date-parts":[[2022,10,20]],"date-time":"2022-10-20T11:14:13Z","timestamp":1666264453000},"page":"52-53","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Impactful research and tooling for program correctness"],"prefix":"10.1145","volume":"65","author":[{"given":"Priyanka","family":"Darke","sequence":"first","affiliation":[{"name":"TATA Consultancy Services Ltd., Pune, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ravindra","family":"Metta","sequence":"additional","affiliation":[{"name":"TATA Consultancy Services Ltd., Pune, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Raveendra Kumar","family":"Medicherla","sequence":"additional","affiliation":[{"name":"TATA Consultancy Services Ltd., Pune, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"R.","family":"Venkatesh","sequence":"additional","affiliation":[{"name":"TATA Consultancy Services Ltd., Pune, India"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,10,20]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proceedings of the Intern. Conf. on Automated Software Engineering","author":"Afzal M.","year":"2019","unstructured":"Afzal, M. et al. VeriAbs: Verification by abstraction and test generation. In Proceedings of the Intern. Conf. on Automated Software Engineering (2019), 1138--1141."},{"key":"e_1_2_1_2_1","volume-title":"Proceedings of the Intern. Conf. Tools and Algorithms for the Construction and Analysis of Systems","author":"Afzal M.","year":"2020","unstructured":"Afzal, M. et al. Veriabs: Verification by abstraction and test generation. In Proceedings of the Intern. Conf. Tools and Algorithms for the Construction and Analysis of Systems (2020), 383--387."},{"key":"e_1_2_1_3_1","volume-title":"Boosting k-induction with continuously refined invariants. CAV","author":"Beyer D.","year":"2015","unstructured":"Beyer, D., Dangl, M., and Wendler, P. Boosting k-induction with continuously refined invariants. CAV (2015), 622--640."},{"volume-title":"Proceedings of the 25th Intern. Conf. Fundamental Approaches to Software Engineering. LNCS 13241","author":"Beyer D.","key":"e_1_2_1_4_1","unstructured":"Beyer, D. Advances in automatic software testing: Test-Comp 2022. In Proceedings of the 25th Intern. Conf. Fundamental Approaches to Software Engineering. LNCS 13241, Springer."},{"key":"e_1_2_1_5_1","volume-title":"Progress on software verification: SV-COMP","author":"Beyer D.","year":"2022","unstructured":"Beyer, D. Progress on software verification: SV-COMP 2022. In Tools and Algorithms for the Construction and Analysis of Systems, LNCS 13244, Springer."},{"key":"e_1_2_1_6_1","unstructured":"C Bounded Model Checker; https:\/\/github.com\/diffblue\/cbmc."},{"key":"e_1_2_1_7_1","volume-title":"Diffy: Inductive reasoning of array programs using difference invariants. Computer Aided Verification","author":"Chakraborty S.","year":"2021","unstructured":"Chakraborty, S., Gupta, A., and Unadkat, D. Diffy: Inductive reasoning of array programs using difference invariants. Computer Aided Verification (2021), 911--935."},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the Intern. Conf. on Languages, Compilers, and Tools for Embedded Systems","author":"Chimdyalwar B.","year":"2018","unstructured":"Chimdyalwar, B. and Darke, P. Statically relating program properties for efficient verification. In Proceedings of the Intern. Conf. on Languages, Compilers, and Tools for Embedded Systems (2018), 99--103."},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the Intern. Conf. Tools and Algorithms for the Construction and Analysis of Systems","author":"Chimdyalwar B.","year":"2017","unstructured":"Chimdyalwar, B. et al. Veriabs: Verification by abstraction. In Proceedings of the Intern. Conf. Tools and Algorithms for the Construction and Analysis of Systems (2017), 457--462."},{"key":"e_1_2_1_10_1","volume-title":"Proceedings of the Intern. Symp. on Formal Methods","author":"Chimdyalwar B.","year":"2015","unstructured":"Chimdyalwar, B. et al. Eliminating static analysis false positives using loop abstraction and bounded model checking. In Proceedings of the Intern. Symp. on Formal Methods (2015), 573--576."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17502-3_22"},{"key":"e_1_2_1_12_1","volume-title":"Proceedings of the Intern. Conf. Tools and Algorithms for the Construction and Analysis of Systems","author":"Darke P.","year":"2021","unstructured":"Darke, P., Agrawal, S., and Venkatesh, R. VeriAbs: A tool for scalable verification by abstraction. In Proceedings of the Intern. Conf. Tools and Algorithms for the Construction and Analysis of Systems (2021)."},{"key":"e_1_2_1_13_1","doi-asserted-by":"crossref","unstructured":"Darke P. et al. Over-approximating loops to prove properties using bounded model checking. Design Automation and Test in Europe Conf. (2015) 1407--1412.","DOI":"10.7873\/DATE.2015.0245"},{"key":"e_1_2_1_14_1","volume-title":"Asia-Pacific Conf. on Software Engineering 2 (December","author":"Darke P.","year":"2012","unstructured":"Darke, P. et al. Precise analysis of large industry code. Asia-Pacific Conf. on Software Engineering 2 (December 2012), 306--309."},{"key":"e_1_2_1_15_1","volume-title":"Proceedings of the Intern. Conf. Tools and Algorithms for the Construction and Analysis of Systems","author":"Darke P.","year":"2018","unstructured":"Darke, P. et al. Veriabs: Verification by abstraction and test generation. In Proceedings of the Intern. Conf. Tools and Algorithms for the Construction and Analysis of Systems (2018), 457--462."},{"volume-title":"Proceedings of IEEE 2017 Intern. Conf. Software Testing, Verification, and Validation, 468--475","author":"Darke P.","key":"e_1_2_1_16_1","unstructured":"Darke, P. et al. Efficient safety proofs for industry-scale code using abstractions and bounded model checking. In Proceedings of IEEE 2017 Intern. Conf. Software Testing, Verification, and Validation, 468--475."},{"key":"e_1_2_1_17_1","volume-title":"Proceedings of the 26th Intern. Symp. on Logic-Based Program Synthesis and Transformation (September","author":"Jana A.","year":"2016","unstructured":"Jana, A. et al. Scaling bounded model checking by transforming programs with arrays. In Proceedings of the 26th Intern. Symp. on Logic-Based Program Synthesis and Transformation (September 2016), 10184. LNCS Springer, 275--292."},{"volume-title":"Proceedings of the 2011 India Software Engineering Conf.","author":"Khare S.","key":"e_1_2_1_18_1","unstructured":"Khare, S., Saraswat, S., and Kumar, S. Static program analysis of large, embedded code base: An experience. In Proceedings of the 2011 India Software Engineering Conf."},{"volume-title":"The cost of poor software quality in the US: A 2020 report","author":"Krasner H.","key":"e_1_2_1_19_1","unstructured":"Krasner, H. The cost of poor software quality in the US: A 2020 report. Consortium for Information and Software Quality; https:\/\/bit.ly\/3QgMN4p."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89960-2_12"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2494569"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.23919\/DATE54114.2022.9774672"},{"key":"e_1_2_1_23_1","volume-title":"Proceedings of the 25th Intern. Conf. on Fundamental Approaches to Software Eng. (April","author":"Metta R.","year":"2022","unstructured":"Metta, R., Medicherla, R.K., and Hrishikesh, K. Verifuzz 1.2: Seeds for fuzzing from BMC with remedies. In Proceedings of the 25th Intern. Conf. on Fundamental Approaches to Software Eng. (April 2022). LNCS 13241, Springer."},{"key":"e_1_2_1_24_1","unstructured":"Zalewski M. American fuzzy lop; http:\/\/lcamtuf.coredump.cx\/afl\/."}],"container-title":["Communications of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3551665","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3551665","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,7]],"date-time":"2025-10-07T00:51:59Z","timestamp":1759798319000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3551665"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,20]]},"references-count":24,"journal-issue":{"issue":"11","published-print":{"date-parts":[[2022,11]]}},"alternative-id":["10.1145\/3551665"],"URL":"https:\/\/doi.org\/10.1145\/3551665","relation":{},"ISSN":["0001-0782","1557-7317"],"issn-type":[{"type":"print","value":"0001-0782"},{"type":"electronic","value":"1557-7317"}],"subject":[],"published":{"date-parts":[[2022,10,20]]},"assertion":[{"value":"2022-10-20","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}