{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:59:15Z","timestamp":1750309155341,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":48,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,6,7]],"date-time":"2022-06-07T00:00:00Z","timestamp":1654560000000},"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":[],"published-print":{"date-parts":[[2022,6,7]]},"DOI":"10.1145\/3611096.3611099","type":"proceedings-article","created":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T23:12:42Z","timestamp":1697497962000},"page":"11-14","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Automated Reasoning Repair"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9031-5599","authenticated-orcid":false,"given":"Amirfarhad","family":"Nilizadeh","sequence":"first","affiliation":[{"name":"Computer Science, University of Central Florida, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3271-3921","authenticated-orcid":false,"given":"Gary T.","family":"Leavens","sequence":"additional","affiliation":[{"name":"Computer Science, University of Central Florida, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1864-4974","authenticated-orcid":false,"given":"David R.","family":"Cok","sequence":"additional","affiliation":[{"name":"Safer Software Consulting, USA"}]}],"member":"320","published-online":{"date-parts":[[2023,10,16]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-019-00501-3"},{"key":"e_1_3_2_1_2_1","volume-title":"Verified Cryptographic Code for Everybody. In International Conference on Computer Aided Verification. Springer, 645\u2013668","author":"Boston Brett","year":"2021","unstructured":"Brett Boston , Samuel Breese , Joey Dodds , Mike Dodds , Brian Huffman , Adam Petcher , and Andrei Stefanescu . 2021 . Verified Cryptographic Code for Everybody. In International Conference on Computer Aided Verification. Springer, 645\u2013668 . Brett Boston, Samuel Breese, Joey Dodds, Mike Dodds, Brian Huffman, Adam Petcher, and Andrei Stefanescu. 2021. Verified Cryptographic Code for Everybody. In International Conference on Computer Aided Verification. Springer, 645\u2013668."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/EUROMICRO.2006.56"},{"key":"e_1_3_2_1_4_1","volume-title":"Proceedings of the International Conference on Software Engineering Research and Practice (SERP\u201902)","author":"Cheon Yoonsik","year":"2002","unstructured":"Yoonsik Cheon and Gary\u00a0 T Leavens . 2002 . A runtime assertion checker for the Java Modeling Language (JML) . In Proceedings of the International Conference on Software Engineering Research and Practice (SERP\u201902) , Las Vegas, Nevada, USA. Citeseer, 322\u2013328. Yoonsik Cheon and Gary\u00a0T Leavens. 2002. A runtime assertion checker for the Java Modeling Language (JML). In Proceedings of the International Conference on Software Engineering Research and Practice (SERP\u201902), Las Vegas, Nevada, USA. Citeseer, 322\u2013328."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_26"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_35"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3464971.3468417"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/MSEC.2022.3153035"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73770-4_10"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3318162"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-60508-7_17"},{"key":"e_1_3_2_1_13_1","volume-title":"Proceedings of the 7th symposium on Operating systems design and implementation. 161\u2013176","author":"Kremenek Ted","year":"2006","unstructured":"Ted Kremenek , Paul Twohey , Godmar Back , Andrew Ng , and Dawson Engler . 2006 . From uncertainty to belief: Inferring the specification within . In Proceedings of the 7th symposium on Operating systems design and implementation. 161\u2013176 . Ted Kremenek, Paul Twohey, Godmar Back, Andrew Ng, and Dawson Engler. 2006. From uncertainty to belief: Inferring the specification within. In Proceedings of the 7th symposium on Operating systems design and implementation. 161\u2013176."},{"key":"e_1_3_2_1_14_1","volume-title":"JML: A Notation for Detailed Design. In Behavioral Specifications of Businesses and Systems, Haim Kilov","author":"Leavens T.","year":"1999","unstructured":"Gary\u00a0 T. Leavens , Albert\u00a0 L. Baker , and Clyde Ruby . 1999 . JML: A Notation for Detailed Design. In Behavioral Specifications of Businesses and Systems, Haim Kilov , Bernhard Rumpe , and Ian Simmonds (Eds.). Kluwer Academic Publishers , Boston, 175\u2013188. Gary\u00a0T. Leavens, Albert\u00a0L. Baker, and Clyde Ruby. 1999. JML: A Notation for Detailed Design. In Behavioral Specifications of Businesses and Systems, Haim Kilov, Bernhard Rumpe, and Ian Simmonds (Eds.). Kluwer Academic Publishers, Boston, 175\u2013188."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1127878.1127884"},{"volume-title":"The Logic of Software. A Tasting Menu of Formal Methods: Essays Dedicated to Reiner H\u00e4hnle on the Occasion of His 60th Birthday","author":"Leavens T","key":"e_1_3_2_1_16_1","unstructured":"Gary\u00a0 T Leavens , David\u00a0 R Cok , and Amirfarhad Nilizadeh . 2022. Further lessons from the JML project . In The Logic of Software. A Tasting Menu of Formal Methods: Essays Dedicated to Reiner H\u00e4hnle on the Occasion of His 60th Birthday . Springer , 313\u2013349. Gary\u00a0T Leavens, David\u00a0R Cok, and Amirfarhad Nilizadeh. 2022. Further lessons from the JML project. In The Logic of Software. A Tasting Menu of Formal Methods: Essays Dedicated to Reiner H\u00e4hnle on the Occasion of His 60th Birthday. Springer, 313\u2013349."},{"key":"e_1_3_2_1_17_1","unstructured":"Gary\u00a0T Leavens Erik Poll Curtis Clifton Yoonsik Cheon Clyde Ruby David Cok Peter M\u00fcller Joseph Kiniry Patrice Chalin Daniel\u00a0M Zimmerman 2008. JML reference manual.  Gary\u00a0T Leavens Erik Poll Curtis Clifton Yoonsik Cheon Clyde Ruby David Cok Peter M\u00fcller Joseph Kiniry Patrice Chalin Daniel\u00a0M Zimmerman 2008. JML reference manual."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2008.08.004"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2017.8115689"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2019.2946563"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2884781.2884807"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.161279"},{"key":"e_1_3_2_1_23_1","volume-title":"Automatic Program Repair Using Formal Verification and Expression Templates. In International Conference on Verification, Model Checking, and Abstract Interpretation. Springer, 70\u201391","author":"Nguyen Thanh-Toan","year":"2019","unstructured":"Thanh-Toan Nguyen , Quang-Trung Ta , and Wei-Ngan Chin . 2019 . Automatic Program Repair Using Formal Verification and Expression Templates. In International Conference on Verification, Model Checking, and Abstract Interpretation. Springer, 70\u201391 . Thanh-Toan Nguyen, Quang-Trung Ta, and Wei-Ngan Chin. 2019. Automatic Program Repair Using Formal Verification and Expression Templates. In International Conference on Verification, Model Checking, and Abstract Interpretation. Springer, 70\u201391."},{"key":"e_1_3_2_1_24_1","volume-title":"Test Overfitting: Challenges, Approaches, and Measurements. Technical Report","author":"Nilizadeh Amirfarhad","year":"2021","unstructured":"Amirfarhad Nilizadeh . 2021 . Test Overfitting: Challenges, Approaches, and Measurements. Technical Report . University of Central Florida , Computer Science . Amirfarhad Nilizadeh. 2021. Test Overfitting: Challenges, Approaches, and Measurements. Technical Report. University of Central Florida, Computer Science."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST53961.2022.00061"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3524482.3527656"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISSRE52982.2021.00032"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3524459.3527346"},{"key":"e_1_3_2_1_29_1","unstructured":"Amirfarhad Nilizadeh Gary\u00a0T Leavens and David\u00a0R Cok. 2023. Toward Using Fuzzers and Lightweight Specs for Semantic Bugs. J. Object Technol. (2023).  Amirfarhad Nilizadeh Gary\u00a0T Leavens and David\u00a0R Cok. 2023. Toward Using Fuzzers and Lightweight Specs for Semantic Bugs. J. Object Technol. (2023)."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST49551.2021.00033"},{"volume-title":"Using a Guided Fuzzer and Preconditions to Achieve Branch Coverage with Valid Inputs","author":"Nilizadeh Amirfarhad","key":"e_1_3_2_1_31_1","unstructured":"Amirfarhad Nilizadeh , Gary\u00a0 T. Leavens , and Corina\u00a0 S. P\u0103s\u0103reanu . 2021. Using a Guided Fuzzer and Preconditions to Achieve Branch Coverage with Valid Inputs . In Tests and Proofs, Fr\u00e9d\u00e9ric Loulergue and Franz Wotawa (Eds.). Springer International Publishing , Cham , 72\u201384. https:\/\/tinyurl.com\/4xzxxrn2 Amirfarhad Nilizadeh, Gary\u00a0T. Leavens, and Corina\u00a0S. P\u0103s\u0103reanu. 2021. Using a Guided Fuzzer and Preconditions to Achieve Branch Coverage with Valid Inputs. In Tests and Proofs, Fr\u00e9d\u00e9ric Loulergue and Franz Wotawa (Eds.). Springer International Publishing, Cham, 72\u201384. https:\/\/tinyurl.com\/4xzxxrn2"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3607538"},{"key":"e_1_3_2_1_33_1","volume-title":"Parameterized Search Heuristic Prediction for Concolic Execution. In 2023 30th Asia-Pacific Software Engineering Conference (APSEC) (In Press). IEEE.","author":"Nilizadeh Farnoushsada","year":"2023","unstructured":"Farnoushsada Nilizadeh , Hamid Dashtbani , and Maryam Mouzarani . 2023 . Parameterized Search Heuristic Prediction for Concolic Execution. In 2023 30th Asia-Pacific Software Engineering Conference (APSEC) (In Press). IEEE. Farnoushsada Nilizadeh, Hamid Dashtbani, and Maryam Mouzarani. 2023. Parameterized Search Heuristic Prediction for Concolic Execution. In 2023 30th Asia-Pacific Software Engineering Conference (APSEC) (In Press). IEEE."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209109"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1858996.1859035"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-88885-5_13"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3464971.3468425"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1390630.1390635"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2015.339"},{"key":"e_1_3_2_1_40_1","unstructured":"Talia Ringer. 2021. Proof Repair. Ph.\u00a0D. Dissertation. University of Washington.  Talia Ringer. 2021. Proof Repair. Ph.\u00a0D. Dissertation. University of Washington."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454033"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167094"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-99725-4_22"},{"key":"e_1_3_2_1_44_1","volume-title":"2018 IEEE\/ACM 40th International Conference on Software Engineering: Companion (ICSE-Companion). IEEE, 313\u2013314","author":"Singleton L","year":"2018","unstructured":"John\u00a0 L Singleton , Gary\u00a0 T Leavens , Hridesh Rajan , and David\u00a0 R. Cok . 2018 . Poster: an algorithm and tool to infer practical postconditions . In 2018 IEEE\/ACM 40th International Conference on Software Engineering: Companion (ICSE-Companion). IEEE, 313\u2013314 . John\u00a0L Singleton, Gary\u00a0T Leavens, Hridesh Rajan, and David\u00a0R. Cok. 2018. Poster: an algorithm and tool to infer practical postconditions. In 2018 IEEE\/ACM 40th International Conference on Software Engineering: Companion (ICSE-Companion). IEEE, 313\u2013314."},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985820"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/1831708.1831716"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2016.2560811"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/SBST.2017.12"}],"event":{"name":"FTfJP '22: 24th ACM International Workshop on Formal Techniques for Java-like Programs","acronym":"FTfJP '22","location":"Berlin Germany"},"container-title":["Proceedings of the 24th ACM International Workshop on Formal Techniques for Java-like Programs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3611096.3611099","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3611096.3611099","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:50:54Z","timestamp":1750287054000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3611096.3611099"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,6,7]]},"references-count":48,"alternative-id":["10.1145\/3611096.3611099","10.1145\/3611096"],"URL":"https:\/\/doi.org\/10.1145\/3611096.3611099","relation":{},"subject":[],"published":{"date-parts":[[2022,6,7]]},"assertion":[{"value":"2023-10-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}