{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:14:50Z","timestamp":1750220090910,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":46,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,5,18]],"date-time":"2022-05-18T00:00:00Z","timestamp":1652832000000},"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,5,18]]},"DOI":"10.1145\/3524482.3527656","type":"proceedings-article","created":{"date-parts":[[2022,7,21]],"date-time":"2022-07-21T22:06:57Z","timestamp":1658441217000},"page":"124-128","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Generating counterexamples in the form of unit tests from hoare-style verification attempts"],"prefix":"10.1145","author":[{"given":"Amirfarhad","family":"Nilizadeh","sequence":"first","affiliation":[{"name":"University of Central Florida"}]},{"given":"Marlon","family":"Calvo","sequence":"additional","affiliation":[{"name":"University of Central Florida"}]},{"given":"Gary T.","family":"Leavens","sequence":"additional","affiliation":[{"name":"University of Central Florida"}]},{"given":"David R.","family":"Cok","sequence":"additional","affiliation":[{"name":"Safer Software Consulting, LLC"}]}],"member":"320","published-online":{"date-parts":[[2022,7,21]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Lecture Notes in Computer Science","volume":"10001","author":"Ahrendt Wolfgang","year":"2016","unstructured":"Wolfgang Ahrendt , Bernhard Beckert , Richard Bubel , Reiner H\u00e4hnle , Peter H. Schmitt , and Mattias Ulbrich ( Eds .). 2016 . Deductive Software Verification - The KeY Book . Lecture Notes in Computer Science , Vol. 10001 . Springer-Verlag, Cham, Switzerland. Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner H\u00e4hnle, Peter H. Schmitt, and Mattias Ulbrich (Eds.). 2016. Deductive Software Verification - The KeY Book. Lecture Notes in Computer Science, Vol. 10001. Springer-Verlag, Cham, Switzerland."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3208071"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-019-00501-3"},{"volume-title":"Fundamentals of Software Engineering","author":"Barbon Gianluca","key":"e_1_3_2_1_4_1","unstructured":"Gianluca Barbon , Vincent Leroy , and Gwen Sala\u00fcn . 2017. Debugging of Concurrent Systems Using Counterexample Analysis . In Fundamentals of Software Engineering , Mehdi Dastani and Marjan Sirjani (Eds.). Springer International Publishing , Cham , 20--34. Gianluca Barbon, Vincent Leroy, and Gwen Sala\u00fcn. 2017. Debugging of Concurrent Systems Using Counterexample Analysis. In Fundamentals of Software Engineering, Mehdi Dastani and Marjan Sirjani (Eds.). Springer International Publishing, Cham, 20--34."},{"key":"e_1_3_2_1_5_1","volume-title":"Schmitt","author":"Beckert Bernhard","year":"2007","unstructured":"Bernhard Beckert , Reiner H\u00e4hnle , and Peter H . Schmitt . 2007 . Verification of Object-Oriented Software: The KeY Approach. Lecture Notes in Computer Science, Vol. 4334 . Springer-Verlag , Berlin. Bernhard Beckert, Reiner H\u00e4hnle, and Peter H. Schmitt. 2007. Verification of Object-Oriented Software: The KeY Approach. Lecture Notes in Computer Science, Vol. 4334. Springer-Verlag, Berlin."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-011-0132-2"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/998675.999437"},{"volume-title":"Fundamental Approaches to Software Engineering, Reiner H\u00e4hnle and Wil van der Aalst (Eds.)","author":"Beyer Dirk","key":"e_1_3_2_1_8_1","unstructured":"Dirk Beyer and Marie-Christine Jakobs . 2019. CoVeriTest: Cooperative Verifier-Based Testing . In Fundamental Approaches to Software Engineering, Reiner H\u00e4hnle and Wil van der Aalst (Eds.) . Springer International Publishing , Cham , 389--408. Dirk Beyer and Marie-Christine Jakobs. 2019. CoVeriTest: Cooperative Verifier-Based Testing. In Fundamental Approaches to Software Engineering, Reiner H\u00e4hnle and Wil van der Aalst (Eds.). Springer International Publishing, Cham, 389--408."},{"key":"e_1_3_2_1_9_1","volume-title":"Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder","author":"Blanchette Jasmin Christian","year":"2010","unstructured":"Jasmin Christian Blanchette and Tobias Nipkow . 2010 . Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder . In Interactive Theorem Proving, Matt Kaufmann and Lawrence C. Paulson (Eds.). Springer, Berlin , Heidelberg , 131--146. Jasmin Christian Blanchette and Tobias Nipkow. 2010. Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder. In Interactive Theorem Proving, Matt Kaufmann and Lawrence C. Paulson (Eds.). Springer, Berlin, Heidelberg, 131--146."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/HASE.2010.15"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.375178"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/566171.566191"},{"key":"e_1_3_2_1_13_1","volume-title":"K Rustan M Leino, and Erik Poll","author":"Burdy Lilian","year":"2005","unstructured":"Lilian Burdy , Yoonsik Cheon , David R Cok , Michael D Ernst , Joseph R Kiniry , Gary T Leavens , K Rustan M Leino, and Erik Poll . 2005 . An overview of JML tools and applications. International journal on software tools for technology transfer 7, 3 (2005), 212--232. Lilian Burdy, Yoonsik Cheon, David R Cok, Michael D Ernst, Joseph R Kiniry, Gary T Leavens, K Rustan M Leino, and Erik Poll. 2005. An overview of JML tools and applications. International journal on software tools for technology transfer 7, 3 (2005), 212--232."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985995"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/217474.217565"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/242223.242257"},{"key":"e_1_3_2_1_17_1","series-title":"Lecture Notes in Computer Science","volume-title":"OpenJML: JML for Java 7 by Extending OpenJDK","author":"Cok David","unstructured":"David Cok . 2011. OpenJML: JML for Java 7 by Extending OpenJDK . In NASA Formal Methods, Mihaela Bobaru, Klaus Havelund, Gerard Holzmann, and Rajeev Joshi (Eds.). Lecture Notes in Computer Science , Vol. 6617 . Springer-Verlag , Berlin , 472--479. https:\/\/tinyurl.com\/3rympeb8 David Cok. 2011. OpenJML: JML for Java 7 by Extending OpenJDK. In NASA Formal Methods, Mihaela Bobaru, Klaus Havelund, Gerard Holzmann, and Rajeev Joshi (Eds.). Lecture Notes in Computer Science, Vol. 6617. Springer-Verlag, Berlin, 472--479. https:\/\/tinyurl.com\/3rympeb8"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3464971.3468417"},{"volume-title":"Formal Reasoning About the Security of Amazon Web Services","author":"Cook Byron","key":"e_1_3_2_1_19_1","unstructured":"Byron Cook . 2018. Formal Reasoning About the Security of Amazon Web Services . In Computer Aided Verification, Hana Chockler and Georg Weissenbacher (Eds.). Springer International Publishing , Cham , 38--47. Byron Cook. 2018. Formal Reasoning About the Security of Amazon Web Services. In Computer Aided Verification, Hana Chockler and Georg Weissenbacher (Eds.). Springer International Publishing, Cham, 38--47."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/960116.54003"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/2773808.2774070"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2025113.2025179"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1002\/1099-1689(200009)10:3<171::AID-STVR209>3.0.CO;2-J"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"volume-title":"Counterexample Interpretation for Contract-Based Design","author":"Kaleeswaran Arut Prakash","key":"e_1_3_2_1_25_1","unstructured":"Arut Prakash Kaleeswaran , Arne Nordmann , Thomas Vogel , and Lars Grunske . 2020. Counterexample Interpretation for Contract-Based Design . In Model-Based Safety and Assessment, Marc Zeller and Kai H\u00f6fig (Eds.). Springer International Publishing , Cham , 99--114. Arut Prakash Kaleeswaran, Arne Nordmann, Thomas Vogel, and Lars Grunske. 2020. Counterexample Interpretation for Contract-Based Design. In Model-Based Safety and Assessment, Marc Zeller and Kai H\u00f6fig (Eds.). Springer International Publishing, Cham, 99--114."},{"key":"e_1_3_2_1_26_1","volume-title":"JML: A Notation for Detailed Design. In Behavioral Specifications of Businesses and Systems, Haim Kilov","author":"Leavens Gary T.","year":"1999","unstructured":"Gary T. Leavens , Albert 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--188. Gary T. Leavens, Albert 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--188."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1127878.1127884"},{"volume-title":"Further Lessons from the JML Project","author":"Leavens Gary T","key":"e_1_3_2_1_28_1","unstructured":"Gary T Leavens , David R Cok , and Amirfarhad Nilizadeh . 2022. Further Lessons from the JML Project . In Festschrift for Reiner H\u00e4hnle (In Press). Springer . Gary T Leavens, David R Cok, and Amirfarhad Nilizadeh. 2022. Further Lessons from the JML Project. In Festschrift for Reiner H\u00e4hnle (In Press). Springer."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2884781.2884807"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.161279"},{"key":"e_1_3_2_1_31_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_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST53961.2022.00061"},{"volume-title":"2021 IEEE 32nd International Symposium on Software Reliability Engineering (ISSRE). IEEE, 208--219","author":"Nilizadeh Amirfarhad","key":"e_1_3_2_1_33_1","unstructured":"Amirfarhad Nilizadeh , Marlon Calvo , Gary T. Leavens , and Xuan-Bach D. Le . 2021. More Reliable Test Suites for Dynamic APR by using Counterexamples . In 2021 IEEE 32nd International Symposium on Software Reliability Engineering (ISSRE). IEEE, 208--219 . Amirfarhad Nilizadeh, Marlon Calvo, Gary T. Leavens, and Xuan-Bach D. Le. 2021. More Reliable Test Suites for Dynamic APR by using Counterexamples. In 2021 IEEE 32nd International Symposium on Software Reliability Engineering (ISSRE). IEEE, 208--219."},{"key":"e_1_3_2_1_34_1","volume-title":"Leavens","author":"Nilizadeh Amirfarhad","year":"2022","unstructured":"Amirfarhad Nilizadeh and Gary T . Leavens . 2022 . Be Realistic : Automated Program Repair is a Combination of Undecidable Problems. In 2022 IEEE\/ACM International Workshop on Automated Program Repair (APR) (In Press) . IEEE. Amirfarhad Nilizadeh and Gary T. Leavens. 2022. Be Realistic: Automated Program Repair is a Combination of Undecidable Problems. In 2022 IEEE\/ACM International Workshop on Automated Program Repair (APR) (In Press). IEEE."},{"volume-title":"2021 14th IEEE Conference on Software Testing, Verification and Validation (ICST). IEEE, 229--240","author":"Nilizadeh Amirfarhad","key":"e_1_3_2_1_35_1","unstructured":"Amirfarhad Nilizadeh , Gary T. Leavens , Xuan-Bach D. Le , Corina S. P\u0103s\u0103reanu , and David R. Cok . 2021. Exploring True Test Overfitting in Dynamic Automated Program Repair using Formal Methods . In 2021 14th IEEE Conference on Software Testing, Verification and Validation (ICST). IEEE, 229--240 . Amirfarhad Nilizadeh, Gary T. Leavens, Xuan-Bach D. Le, Corina S. P\u0103s\u0103reanu, and David R. Cok. 2021. Exploring True Test Overfitting in Dynamic Automated Program Repair using Formal Methods. In 2021 14th IEEE Conference on Software Testing, Verification and Validation (ICST). IEEE, 229--240."},{"key":"e_1_3_2_1_36_1","volume-title":"P\u0103s\u0103reanu","author":"Nilizadeh Amirfarhad","year":"2021","unstructured":"Amirfarhad Nilizadeh , Gary T. Leavens , and Corina 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--84. https:\/\/tinyurl.com\/4xzxxrn2 Amirfarhad Nilizadeh, Gary T. Leavens, and Corina 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--84. https:\/\/tinyurl.com\/4xzxxrn2"},{"volume-title":"Companion to the 22nd ACM SIGPLAN conference on Object-oriented programming systems and applications companion. 815--816.","author":"Pacheco Carlos","key":"e_1_3_2_1_37_1","unstructured":"Carlos Pacheco and Michael D Ernst . 2007. Randoop: feedback-directed random testing for Java . In Companion to the 22nd ACM SIGPLAN conference on Object-oriented programming systems and applications companion. 815--816. Carlos Pacheco and Michael D Ernst. 2007. Randoop: feedback-directed random testing for Java. In Companion to the 22nd ACM SIGPLAN conference on Object-oriented programming systems and applications companion. 815--816."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2401603.2401682"},{"key":"e_1_3_2_1_39_1","volume-title":"Perfect Is the Enemy of Good: Best-Effort Program Synthesis. In 34th European Conference on Object-Oriented Programming (ECOOP 2020) (Leibniz International Proceedings in Informatics (LIPIcs)","volume":"30","author":"Peleg Hila","year":"2020","unstructured":"Hila Peleg and Nadia Polikarpova . 2020 . Perfect Is the Enemy of Good: Best-Effort Program Synthesis. In 34th European Conference on Object-Oriented Programming (ECOOP 2020) (Leibniz International Proceedings in Informatics (LIPIcs) , Vol. 166), Robert Hirschfeld and Tobias Pape (Eds.). Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany, 2:1--2: 30 . Hila Peleg and Nadia Polikarpova. 2020. Perfect Is the Enemy of Good: Best-Effort Program Synthesis. In 34th European Conference on Object-Oriented Programming (ECOOP 2020) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 166), Robert Hirschfeld and Tobias Pape (Eds.). Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany, 2:1--2:30."},{"volume-title":"Teaching Program Specification and Verification Using JML and ESC\/Java2","author":"Poll Erik","key":"e_1_3_2_1_40_1","unstructured":"Erik Poll . 2009. Teaching Program Specification and Verification Using JML and ESC\/Java2 . In Teaching Formal Methods, Jeremy Gibbons and Jos\u00e9 Nuno Oliveira (Eds.). Springer , Berlin, Heidelberg , 92--104. Erik Poll. 2009. Teaching Program Specification and Verification Using JML and ESC\/Java2. In Teaching Formal Methods, Jeremy Gibbons and Jos\u00e9 Nuno Oliveira (Eds.). Springer, Berlin, Heidelberg, 92--104."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2786825"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.12.027"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1831708.1831716"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2016.2560811"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/SBST.2017.12"},{"volume-title":"JMLUnit: The Next Generation. In International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2010)","author":"Daniel","key":"e_1_3_2_1_46_1","unstructured":"Daniel M. Zimmerman and Rinkesh Nagmoti. 2010 . JMLUnit: The Next Generation. In International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2010) (Paris, France). Springer-Verlag, Berlin, 183--197. Daniel M. Zimmerman and Rinkesh Nagmoti. 2010. JMLUnit: The Next Generation. In International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2010) (Paris, France). Springer-Verlag, Berlin, 183--197."}],"event":{"name":"FormaliSE '22: International Conference on Formal Methods in Software Engineering","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","IEEE CS"],"location":"Pittsburgh Pennsylvania","acronym":"FormaliSE '22"},"container-title":["Proceedings of the IEEE\/ACM 10th International Conference on Formal Methods in Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3524482.3527656","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3524482.3527656","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:09:51Z","timestamp":1750183791000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3524482.3527656"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,5,18]]},"references-count":46,"alternative-id":["10.1145\/3524482.3527656","10.1145\/3524482"],"URL":"https:\/\/doi.org\/10.1145\/3524482.3527656","relation":{},"subject":[],"published":{"date-parts":[[2022,5,18]]},"assertion":[{"value":"2022-07-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}