{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,11]],"date-time":"2026-05-11T11:19:39Z","timestamp":1778498379110,"version":"3.51.4"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031098260","type":"print"},{"value":"9783031098277","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-09827-7_5","type":"book-chapter","created":{"date-parts":[[2022,6,21]],"date-time":"2022-06-21T16:46:47Z","timestamp":1655830007000},"page":"69-88","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Fuzzing and\u00a0Delta Debugging And-Inverter Graph Verification Tools"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5645-0292","authenticated-orcid":false,"given":"Daniela","family":"Kaufmann","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7170-9242","authenticated-orcid":false,"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,6,22]]},"reference":[{"key":"5_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-642-38916-0_3","volume-title":"Tests and Proofs","author":"C Artho","year":"2013","unstructured":"Artho, C., Biere, A., Seidl, M.: Model-based testing for verification back-ends. In: Veanes, M., Vigan\u00f2, L. (eds.) TAP 2013. LNCS, vol. 7942, pp. 39\u201355. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38916-0_3"},{"key":"5_CR2","unstructured":"Biere, A., Heljanko, K., Wieringa, S.: AIGER 1.9 And Beyond. Technical report, FMV Reports Series, JKU Linz, Austria (2011)"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/978-3-319-96142-2_6","volume-title":"Computer Aided Verification","author":"D Blotsky","year":"2018","unstructured":"Blotsky, D., Mora, F., Berzish, M., Zheng, Y., Kabir, I., Ganesh, V.: StringFuzz: a fuzzer for string solvers. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 45\u201351. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_6"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"Brummayer, R., Biere, A.: Fuzzing and delta-debugging SMT solvers. In: SMT Workshop, SMT 2009, pp. 1\u20135, New York, Association for Computing Machinery (2009)","DOI":"10.1145\/1670412.1670413"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/978-3-642-14186-7_6","volume-title":"Theory and Applications of Satisfiability Testing","author":"R Brummayer","year":"2010","unstructured":"Brummayer, R., Lonsing, F., Biere, A.: Automated testing and debugging of SAT and QBF solvers. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 44\u201357. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14186-7_6"},{"issue":"6","key":"5_CR6","first-page":"1346","volume":"39","author":"MJ Ciesielski","year":"2019","unstructured":"Ciesielski, M.J., Su, T., Yasin, A., Yu, C.: Understanding Algebraic rewriting for arithmetic circuit verification: a bit-flow model. IEEE TCAD 39(6), 1346\u20131357 (2019)","journal-title":"IEEE TCAD"},{"key":"5_CR7","unstructured":"Godefroid, P., Levin, M.Y., Molnar, D.A.: Automated whitebox fuzz testing. The Internet Society In NDSS (2008)"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"Herfert, S., Patra, J., Pradel, M.: Automatically reducing tree-structured test inputs. In: ASE, pp. 861\u2013871. IEEE Computer Society (2017)","DOI":"10.1109\/ASE.2017.8115697"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"Homma, N., Watanabe, Y., Aoki, T., Higuchi, T.: Formal Design of arithmetic circuits based on arithmetic description language. IEICE Trans. 89-A(12), 3500\u20133509 (2006)","DOI":"10.1093\/ietfec\/e89-a.12.3500"},{"key":"5_CR10","unstructured":"Kaufmann, D.: Amulet 2.1. https:\/\/github.com\/d-kfmnn\/amulet. SHA 8e1838fa4c6d80091869407c44519e2771694b21"},{"key":"5_CR11","unstructured":"Kaufmann, D.: Formal Verification of Multiplier Circuits using Computer Algebra. PhD thesis, Computer Science, Johannes Kepler University Linz (2020)"},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"Kaufmann, D.: Artifact for fuzzing and delta-debugging and-inverter graph verification tools (2022). http:\/\/fmv.jku.at\/aigfuzzing_artifact","DOI":"10.1007\/978-3-031-09827-7_5"},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-030-72013-1_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Kaufmann","year":"2021","unstructured":"Kaufmann, D., Biere, A.: AMulet\u00a02.0 for verifying multiplier circuits. In: TACAS 2021. LNCS, vol. 12652, pp. 357\u2013364. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_19"},{"key":"5_CR14","unstructured":"Kaufmann, D., Biere, A., Kauers, M.: Verifying SAT and computer algebra. In: FMCAD 2019, pp. 28\u201336. IEEE (2019)"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Kaufmann, D., Fleury, M., Biere, A., Kauers, M.: Practical algebraic calculus and nullstellensatz with the checkers pacheck and past\u00e8que and nuss-checker. Formal Methods Syst. Des., 35 p. (2022, online first). https:\/\/doi.org\/10.1007\/s10703-022-00391-x","DOI":"10.1007\/s10703-022-00391-x"},{"key":"5_CR16","unstructured":"Kaufmann, D., Kauers, M., Biere, A., Cok, D.: Arithmetic verification problems submitted to the SAT race 2019. In: SAT Race 2019, volume B-2019-1 of Dep. of Computer Science Report Series B, p. 49. University of Helsinki, (2019)"},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-030-81688-9_11","volume-title":"Computer Aided Verification","author":"G Kremer","year":"2021","unstructured":"Kremer, G., Niemetz, A., Preiner, M.: ddSMT 2.0: better delta debugging for the SMT-LIBv2 language and friends. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 231\u2013242. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_11"},{"issue":"12","key":"5_CR18","first-page":"1377","volume":"21","author":"A Kuehlmann","year":"2002","unstructured":"Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.: Robust Boolean reasoning for equivalence checking and functional property verification. IEEE TCAD 21(12), 1377\u20131394 (2002)","journal-title":"IEEE TCAD"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"Lampropoulos, L., Hicks, M., Pierce, B.C.: Coverage guided, property based testing. Proc. ACM Program. Lang. 3(OOPSLA), 181:1\u2013181:29 (2019)","DOI":"10.1145\/3360607"},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"Mahzoon, A., Gro\u00dfe, D., Drechsler, R.: RevSCA: using reverse engineering to bring light into backward rewriting for big and dirty multipliers. In: DAC 2019, pp. 185:1\u2013185:6. ACM (2019)","DOI":"10.1145\/3316781.3317898"},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"Mahzoon, A., Gro\u00dfe, D., Scholl, C., Drechsler, R.: Towards formal verification of optimized and industrial multipliers. In: DATE, pp. 544\u2013549. IEEE (2020)","DOI":"10.23919\/DATE48585.2020.9116485"},{"key":"5_CR22","unstructured":"A. Mahzoon, D. Gro\u00dfe, and R. Drechsler. Multiplier Generator GenMul (2019). http:\/\/www.sca-verification.org\/"},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"Mansur, M.N., Christakis, M., W\u00fcstholz, V., Zhang, F.: Detecting critical bugs in SMT solvers using blackbox mutational fuzzing. In: ESEC\/SIGSOFT FSE, pp. 701\u2013712. ACM (2020)","DOI":"10.1145\/3368089.3409763"},{"issue":"1","key":"5_CR24","first-page":"100","volume":"10","author":"WM McKeeman","year":"1998","unstructured":"McKeeman, W.M.: Differential testing for software. Digit. Tech. J. 10(1), 100\u2013107 (1998)","journal-title":"Digit. Tech. J."},{"key":"5_CR25","doi-asserted-by":"crossref","unstructured":"B. Miller, M. Zhang, and E. Heymann. The relevance of classic fuzz testing: have we solved this one? IEEE Trans. Softw. Eng. 1 (2020, early acces). https:\/\/doi.org\/10.1109\/TSE.2020.3047766","DOI":"10.1109\/TSE.2020.3047766"},{"issue":"12","key":"5_CR26","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1145\/96267.96279","volume":"33","author":"BP Miller","year":"1990","unstructured":"Miller, B.P., Fredriksen, L., So, B.: An empirical study of the reliability of unix utilities. Commun. ACM 33(12), 32\u201344 (1990)","journal-title":"Commun. ACM"},{"key":"5_CR27","unstructured":"Niemetz, A., Biere, A.: ddSMT: a delta debugger for the SMT-LIB v2 Format. In: Bruttomesso, R., Griggio, A. (eds.), Proceedings of the 11th International Workshop on Satisfiability Modulo Theories, SMT 2013), affiliated with the 16th International Conference on Theory and Applications of Satisfiability Testing, SAT 2013, Helsinki, Finland, 8\u20139 July 2013, pp. 36\u201345 (2013)"},{"key":"5_CR28","unstructured":"Niemetz, A., Preiner, M., Biere, A.: Model-based API testing for SMT solvers. In: SMT, volume 1889 of CEUR Workshop Proceedings, pp. 3\u201314. CEUR-WS.org (2017)"},{"key":"5_CR29","unstructured":"Parhami, B.: Computer Arithmetic - Algorithms and Hardware designs. Oxford University Press, Oxford (2000)"},{"key":"5_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-030-90870-6_6","volume-title":"Formal Methods","author":"J Scott","year":"2021","unstructured":"Scott, J., Sudula, T., Rehman, H., Mora, F., Ganesh, V.: BanditFuzz: fuzzing SMT solvers with multi-agent reinforcement learning. In: Huisman, M., P\u0103s\u0103reanu, C., Zhan, N. (eds.) FM 2021. LNCS, vol. 13047, pp. 103\u2013121. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-90870-6_6"},{"key":"5_CR31","unstructured":"Sharangpani, H., Barton, M.L.: Statistical analysis of floating point flaw in the pentium processor. In: Technical Report Intel Corporation (1994)"},{"key":"5_CR32","unstructured":"Temel, M.: MultGen. https:\/\/github.com\/temelmertcan\/multgen (2020). SHA 32f4eb1bff419a88f02035d365d88089f6c33e5f"},{"key":"5_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/3-540-48166-4_16","volume-title":"Software Engineering","author":"A Zeller","year":"1999","unstructured":"Zeller, A.: Yesterday, my program worked. today, it does not. why? In: Nierstrasz, O., Lemoine, M. (eds.) ESEC\/SIGSOFT FSE -1999. LNCS, vol. 1687, pp. 253\u2013267. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48166-4_16"},{"key":"5_CR34","unstructured":"Zeller, A.: The Debugging Book. CISPA Helmholtz Center for Information Security (2021)"},{"key":"5_CR35","unstructured":"Zeller, A., Gopinath, R., B\u00f6hme, M., Fraser, G., Holler, C.: The Fuzzing Book. CISPA Helmholtz Center for Information Security (2021)"},{"issue":"2","key":"5_CR36","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1109\/32.988498","volume":"28","author":"A Zeller","year":"2002","unstructured":"Zeller, A., Hildebrandt, R.: Simplifying and isolating failure-inducing input. IEEE Trans. Softw. Eng. 28(2), 183\u2013200 (2002)","journal-title":"IEEE Trans. Softw. Eng."}],"container-title":["Lecture Notes in Computer Science","Tests and Proofs"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-09827-7_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,6,23]],"date-time":"2022-06-23T23:14:10Z","timestamp":1656026050000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-09827-7_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031098260","9783031098277"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-09827-7_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"22 June 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TAP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tests and Proofs","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Nantes","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 July 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 July 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tap2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/easychair.org\/smart-program\/TAP22\/index.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"1","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"55% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}