{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T21:15:32Z","timestamp":1770239732520,"version":"3.49.0"},"reference-count":46,"publisher":"Association for Computing Machinery (ACM)","issue":"FSE","license":[{"start":{"date-parts":[[2024,7,12]],"date-time":"2024-07-12T00:00:00Z","timestamp":1720742400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Proc. ACM Softw. Eng."],"published-print":{"date-parts":[[2024,7,12]]},"abstract":"<jats:p>\n                    Model checking has been used traditionally for finding violations of temporal properties. Recently, testing or fuzzing approaches have also been applied to software systems to find temporal property violations. However, model checking suffers from state explosion, while fuzzing can only partially cover program paths. Moreover, once a violation is found, the fix for the temporal error is usually manual. In this work, we develop the first compositional static analyzer for temporal properties, and the analyzer supports a proof-based repair strategy to fix temporal bugs automatically. To enable a more flexible specification style for temporal properties, on top of the classic pre\/post-conditions, we allow users to write a\n                    <jats:italic toggle=\"yes\">future<\/jats:italic>\n                    -condition to modularly express the expected behaviors after the function call. Instead of requiring users to write specifications for each procedure, our approach automatically infers the procedure\u2019s specification according to user-supplied specifications for a small number of primitive APIs. We further devise a term rewriting system to check the actual behaviors against its inferred specification. Our method supports the analysis of 1) memory usage bugs, 2) unchecked return values, 3) resource leaks, etc., with annotated specifications for 17 primitive APIs, and detects 515 vulnerabilities from over 1 million lines of code ranging from ten real-world C projects. Intuitively, the benefit of our approach is that a small set of properties can be specified once and used to analyze\/repair a large number of programs. Experimental results show that our tool, P\n                    <jats:sc>rove<\/jats:sc>\n                    NF\n                    <jats:sc>ix<\/jats:sc>\n                    , detects\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:mrow>\n                          <mml:mn>72.2<\/mml:mn>\n                          <mml:mi>%<\/mml:mi>\n                        <\/mml:mrow>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    more true alarms than the latest release of the Infer static analyzer. Moreover, we show the effectiveness of our repair strategy when compared to other state-of-the-art systems \u2014 fixing\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:mrow>\n                          <mml:mn>5<\/mml:mn>\n                          <mml:mi>%<\/mml:mi>\n                        <\/mml:mrow>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    more memory leaks than SAVER,\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:mrow>\n                          <mml:mn>40<\/mml:mn>\n                          <mml:mi>%<\/mml:mi>\n                        <\/mml:mrow>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    more resource leaks than FootPatch, and with a\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:mrow>\n                          <mml:mn>90<\/mml:mn>\n                          <mml:mi>%<\/mml:mi>\n                        <\/mml:mrow>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    fix rate for null pointer dereferences.\n                  <\/jats:p>","DOI":"10.1145\/3643737","type":"journal-article","created":{"date-parts":[[2024,7,12]],"date-time":"2024-07-12T10:22:09Z","timestamp":1720779729000},"page":"226-248","source":"Crossref","is-referenced-by-count":8,"title":["ProveNFix: Temporal Property-Guided Program Repair"],"prefix":"10.1145","volume":"1","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9760-5895","authenticated-orcid":false,"given":"Yahui","family":"Song","sequence":"first","affiliation":[{"name":"National University of Singapore, Singapore, Singapore"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9895-4600","authenticated-orcid":false,"given":"Xiang","family":"Gao","sequence":"additional","affiliation":[{"name":"Beihang University, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-9479-8061","authenticated-orcid":false,"given":"Wenhua","family":"Li","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore, Singapore"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9660-5682","authenticated-orcid":false,"given":"Wei-Ngan","family":"Chin","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore, Singapore"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7127-1137","authenticated-orcid":false,"given":"Abhik","family":"Roychoudhury","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore, Singapore"}]}],"member":"320","published-online":{"date-parts":[[2024,7,12]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054109006802"},{"key":"e_1_3_1_3_2","first-page":"455","volume-title":"Annual Symposium on Theoretical Aspects of Computer Science","author":"Antimirov Valentin","year":"1995","unstructured":"Valentin Antimirov. 1995. Partial derivatives of regular expressions and finite automata constructions. In Annual Symposium on Theoretical Aspects of Computer Science. Springer, 455\u2013466."},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)80024-4"},{"key":"e_1_3_1_5_2","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1007\/978-3-642-22110-1_16","volume-title":"Computer Aided Verification: 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings 23","author":"Beyer Dirk","year":"2011","unstructured":"Dirk Beyer and M Erkan Keremoglu. 2011. CPAchecker: A tool for configurable software verification. In Computer Aided Verification: 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings 23. Springer, 184\u2013190."},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-17524-9_1"},{"key":"e_1_3_1_7_2","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification: 14th International Conference, CAV 2002 Copenhagen, Denmark, July 27\u201331, 2002 Proceedings 14","author":"Cimatti Alessandro","year":"2002","unstructured":"Alessandro Cimatti, Edmund Clarke, Enrico Giunchiglia, Fausto Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, and Armando Tacchella. 2002. Nusmv 2: An opensource tool for symbolic model checking. In Computer Aided Verification: 14th International Conference, CAV 2002 Copenhagen, Denmark, July 27\u201331, 2002 Proceedings 14. Springer, 359\u2013364."},{"key":"e_1_3_1_8_2","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1007\/BFb0058022","volume-title":"Foundations of Software Technology and Theoretical Computer Science: 17th Conference Kharagpur, India, December 18\u201320, 1997 Proceedings 17","author":"Clarke Edmund M","year":"1997","unstructured":"Edmund M Clarke. 1997. Model checking. In Foundations of Software Technology and Theoretical Computer Science: 17th Conference Kharagpur, India, December 18\u201320, 1997 Proceedings 17. Springer, 54\u201356."},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35746-6_1"},{"key":"e_1_3_1_10_2","unstructured":"CVE-2016-2113. 2016. CVE-2016-2113. https:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2016-2113."},{"key":"e_1_3_1_11_2","doi-asserted-by":"crossref","unstructured":"Cve-2016-2182. 2016. Cve-2016-2182. https:\/\/nvd.nist.gov\/vuln\/detail\/CVE-2016-2182.","DOI":"10.1149\/MA2016-02\/34\/2182"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-17524-9_13"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/2382196.2382204"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.18293\/SEKE2019-006"},{"key":"e_1_3_1_16_2","doi-asserted-by":"crossref","unstructured":"Sim\u00f3n Guti\u00e9rrez Brida Germ\u00e1n Regis Guolong Zheng Hamid Bagheri ThanhVu Nguyen Nazareno Aguirre and Marcelo Frias. 2021. Bounded Exhaustive Search of Alloy Specification Repairs. In 2021 IEEE\/ACM 43rd International Conference on Software Engineering (ICSE).","DOI":"10.1109\/ICSE43902.2021.00105"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/3377811.3380323"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2011.12.003"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00071"},{"key":"e_1_3_1_21_2","doi-asserted-by":"crossref","first-page":"692","DOI":"10.1007\/978-3-662-46681-0_61","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems: 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings 21","author":"Kant Gijs","year":"2015","unstructured":"Gijs Kant, Alfons Laarman, Jeroen Meijer, Jaco Van de Pol, Stefan Blom, and Tom Van Dijk. 2015. LTSmin: high-performance language-independent model checking. In Tools and Algorithms for the Construction and Analysis of Systems: 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings 21. Springer, 692\u2013707."},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSTTCS.2014.175"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_13"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/3527325"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/3236024.3236079"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/2970276.2970356"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/3510003.3510082"},{"key":"e_1_3_1_28_2","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1145\/844128.844136","article-title":"CMC: A pragmatic approach to model checking real code","volume":"36","author":"Musuvathi Madanlal","year":"2002","unstructured":"Madanlal Musuvathi, David YW Park, Andy Chou, Dawson R Engler, and David L Dill. 2002. CMC: A pragmatic approach to model checking real code. ACM SIGOPS Operating Systems Review 36, SI (2002), 75\u201388.","journal-title":"ACM SIGOPS Operating Systems Review"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-67067-2_17"},{"key":"e_1_3_1_30_2","unstructured":"openssl. 2019. Openssl: cryptography and ssl\/tls toolkit. https:\/\/github.com\/openssl\/."},{"key":"e_1_3_1_31_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2014.2312918"},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290385"},{"key":"e_1_3_1_33_2","unstructured":"Swoole Project. [n.d.]. Swoole Project. https:\/\/github.com\/swoole\/swoole-src."},{"key":"e_1_3_1_34_2","doi-asserted-by":"crossref","first-page":"596","DOI":"10.1007\/978-3-662-46681-0_55","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems: 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings 21","author":"Reger Giles","year":"2015","unstructured":"Giles Reger, Helena Cuenca Cruz, and David Rydeheard. 2015. MarQ: monitoring at runtime with QEA. In Tools and Algorithms for the Construction and Analysis of Systems: 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings 21. Springer, 596\u2013610."},{"key":"e_1_3_1_35_2","first-page":"593","volume-title":"FM 2016: Formal Methods: 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings 21","author":"Rothenberg Bat-Chen","year":"2016","unstructured":"Bat-Chen Rothenberg and Orna Grumberg. 2016. Sound and complete mutation-based program repair. In FM 2016: Formal Methods: 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings 21. Springer, 593\u2013611."},{"key":"e_1_3_1_36_2","volume-title":"Two approaches to interprocedural data flow analysis","author":"Sharir Micha","year":"1978","unstructured":"Micha Sharir, Amir Pnueli, et al. 1978. Two approaches to interprocedural data flow analysis. New York University. Courant Institute of Mathematical Sciences"},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-63406-3_5"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-67067-2_19"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30823-9_29"},{"key":"e_1_3_1_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-21037-2_5"},{"key":"e_1_3_1_41_2","first-page":"868","article-title":"Runtime Monitoring with Union-Find Structures","volume":"9636","author":"Thoma Daniel","unstructured":"Daniel Thoma. [n.d.]. Runtime Monitoring with Union-Find Structures. Tools and Algorithms for the Construction and Analysis of Systems LNCS 9636 ([n. d.]), 868.","journal-title":"Tools and Algorithms for the Construction and Analysis of Systems LNCS"},{"key":"e_1_3_1_42_2","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180250"},{"key":"e_1_3_1_43_2","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1007\/11537328_5","volume-title":"Model Checking Software: 12th International SPIN Workshop","author":"Visser Willem","year":"2005","unstructured":"Willem Visser and Peter Mehlitz. 2005. Model checking programs with Java PathFinder. In Model Checking Software: 12th International SPIN Workshop. Springer, 27\u201327."},{"key":"e_1_3_1_44_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(83)80051-5"},{"key":"e_1_3_1_45_2","doi-asserted-by":"publisher","DOI":"10.1109\/ISSRE.2004.11"},{"key":"e_1_3_1_46_2","doi-asserted-by":"publisher","DOI":"10.1145\/996821.996832"},{"key":"e_1_3_1_47_2","doi-asserted-by":"publisher","unstructured":"Zenodo. 2023. Benchmark and Source Code. https:\/\/doi.org\/10.5281\/zenodo.8388488 10.5281\/zenodo.8388488.","DOI":"10.5281\/zenodo.8388488"}],"container-title":["Proceedings of the ACM on Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3643737","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3643737","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T07:52:35Z","timestamp":1770191555000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3643737"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,7,12]]},"references-count":46,"journal-issue":{"issue":"FSE","published-print":{"date-parts":[[2024,7,12]]}},"alternative-id":["10.1145\/3643737"],"URL":"https:\/\/doi.org\/10.1145\/3643737","relation":{},"ISSN":["2994-970X"],"issn-type":[{"value":"2994-970X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,7,12]]}}}