{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,5]],"date-time":"2026-07-05T21:52:37Z","timestamp":1783288357100,"version":"3.54.6"},"publisher-location":"New York, NY, USA","reference-count":46,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,10,27]],"date-time":"2024-10-27T00:00:00Z","timestamp":1729987200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["101076510"],"award-info":[{"award-number":["101076510"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,10,27]]},"DOI":"10.1145\/3691620.3695034","type":"proceedings-article","created":{"date-parts":[[2024,10,18]],"date-time":"2024-10-18T15:39:19Z","timestamp":1729265959000},"page":"319-330","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Interrogation Testing of Program Analyzers for Soundness and Precision Issues"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-4137-5163","authenticated-orcid":false,"given":"David","family":"Kaindlstorfer","sequence":"first","affiliation":[{"name":"TU Wien, Vienna, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6375-0421","authenticated-orcid":false,"given":"Anastasia","family":"Isychev","sequence":"additional","affiliation":[{"name":"TU Wien, Vienna, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1496-1104","authenticated-orcid":false,"given":"Valentin","family":"W\u00fcstholz","sequence":"additional","affiliation":[{"name":"ConsenSys, Vienna, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2649-1958","authenticated-orcid":false,"given":"Maria","family":"Christakis","sequence":"additional","affiliation":[{"name":"TU Wien, Vienna, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,10,27]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"[n. d.]. C-Reduce A C and C++ Program Reducer. https:\/\/github.com\/csmith-project\/creduce."},{"key":"e_1_3_2_1_2_1","unstructured":"[n.d.]. Goblint. https:\/\/github.com\/goblint\/analyzer."},{"key":"e_1_3_2_1_3_1","unstructured":"[n.d.]. Technical \"Whitepaper\" for AFL. http:\/\/lcamtuf.coredump.cx\/afl\/technical_details.txt."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Dirk Beyer. 2012. Competition on Software Verification (SV-COMP). https:\/\/sv-comp.sosy-lab.org.","DOI":"10.1007\/978-3-642-36742-7_43"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"crossref","unstructured":"Dirk Beyer. 2019. Competition on Software Testing (Test-COMP). https:\/\/test-comp.sosy-lab.org.","DOI":"10.1007\/978-3-030-17502-3_11"},{"key":"e_1_3_2_1_6_1","volume-title":"CAV (LNCS","author":"Beyer Dirk","unstructured":"Dirk Beyer and M. Erkan Keremoglu. 2011. CPAchecker: A Tool for Configurable Software Verification. In CAV (LNCS, Vol. 6806). Springer, 184--190."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.21236\/ADA360973"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Alexandra Bugariu and Peter M\u00fcller. 2020. Automatically Testing String Solvers. In ICSE. ACM 1459--1470.","DOI":"10.1145\/3377811.3380398"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"crossref","unstructured":"Alexandra Bugariu Valentin W\u00fcstholz Maria Christakis and Peter M\u00fcller. 2018. Automatically Testing Implementations of Numerical Abstract Domains. In ASE. ACM 768--778.","DOI":"10.1145\/3238147.3240464"},{"key":"e_1_3_2_1_10_1","volume-title":"Engler","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar, Daniel Dunbar, and Dawson R. Engler. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In OSDI. USENIX, 209--224."},{"key":"e_1_3_2_1_11_1","first-page":"82","article-title":"Symbolic Execution for Software Testing","volume":"56","author":"Cadar Cristian","year":"2013","unstructured":"Cristian Cadar and Koushik Sen. 2013. Symbolic Execution for Software Testing: Three Decades Later. CACM 56 (2013), 82--90. Issue 2.","journal-title":"Three Decades Later. CACM"},{"key":"e_1_3_2_1_12_1","first-page":"1","article-title":"A Survey of Compiler","volume":"53","author":"Chen Junjie","year":"2020","unstructured":"Junjie Chen, Jibesh Patra, Michael Pradel, Yingfei Xiong, Hongyu Zhang, Dan Hao, and Lu Zhang. 2020. A Survey of Compiler Testing. Comput. Surv. 53 (2020), 4:1--4:36. Issue 1.","journal-title":"Testing. Comput. Surv."},{"key":"e_1_3_2_1_13_1","volume-title":"Metamorphic Testing: A New Approach for Generating Next Test Cases. Technical Report HKUST-CS98-01. HKUST.","author":"Chen Tsong Yueh","year":"1998","unstructured":"Tsong Yueh Chen, S. C. Cheung, and Siu-Ming Yiu. 1998. Metamorphic Testing: A New Approach for Generating Next Test Cases. Technical Report HKUST-CS98-01. HKUST."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"crossref","unstructured":"Maria Christakis and Christian Bird. 2016. What Developers Want and Need from Program Analysis: An Empirical Study. In ASE. ACM 332--343.","DOI":"10.1145\/2970276.2970347"},{"key":"e_1_3_2_1_15_1","volume-title":"andFlavio Lerda","author":"Clarke Edmund M.","year":"2004","unstructured":"Edmund M. Clarke, Daniel Kroening, andFlavio Lerda. 2004. A Tool for Checking ANSI-C Programs. In TACAS (LNCS, Vol. 2988). Springer, 168--176."},{"key":"e_1_3_2_1_16_1","volume-title":"SMT-Based Bounded Model Checking for Embedded ANSI-C Software","author":"Cordeiro Lucas C.","unstructured":"Lucas C. Cordeiro, Bernd Fischer, and Jo\u00e3o Marques-Silva. 2009. SMT-Based Bounded Model Checking for Embedded ANSI-C Software. In ASE. IEEE Computer Society, 137--148."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"crossref","unstructured":"Karine Even-Mendoza Arindam Sharma Alastair F. Donaldson and Cristian Cadar. 2023. GrayC: Greybox Fuzzing of Compilers and Analysers for C. In ISSTA. ACM 1219--1231.","DOI":"10.1145\/3597926.3598130"},{"key":"e_1_3_2_1_19_1","volume-title":"Navas","author":"Gurfinkel Arie","year":"2021","unstructured":"Arie Gurfinkel and Jorge A. Navas. 2021. Abstract Interpretation of LLVM with a Region-Based Memory Model. In VSTTE (LNCS, Vol. 13124). Springer, 122--144."},{"key":"e_1_3_2_1_20_1","first-page":"1656","article-title":"Finding and Understanding Defects in Static Analyzers by Constructing Automated Oracles","volume":"1","author":"He Weigang","year":"2024","unstructured":"Weigang He, Peng Di, Mengli Ming, Chengyu Zhang, Ting Su, Shijie Li, and Yulei Sui. 2024. Finding and Understanding Defects in Static Analyzers by Constructing Automated Oracles. PACMSE 1 (2024), 1656--1678. Issue FSE.","journal-title":"PACMSE"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03237-0_7"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_2"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"crossref","unstructured":"Ahmed Irfan Sorawee Porncharoenwase Zvonimir Rakamaric Neha Rungta and Emina Torlak. 2022. Testing Dafny (experience paper). In ISSTA. ACM 556--567.","DOI":"10.1145\/3533767.3534382"},{"key":"e_1_3_2_1_24_1","volume-title":"VSTTE (LNCS","volume":"18","author":"Journault Matthieu","year":"2019","unstructured":"Matthieu Journault, Antoine Min\u00e9, Rapha\u00ebl Monat, and Abdelraouf Ouadjaout. 2019. Combinations of Reusable Abstract Domains for a Multilingual Static Analyzer. In VSTTE (LNCS, Vol. 12031). Springer, 1--18."},{"key":"e_1_3_2_1_25_1","volume-title":"Automatic Testing of Symbolic Execution Engines via Program Generation and Differential Testing","author":"Kapus Timotej","unstructured":"Timotej Kapus and Cristian Cadar. 2017. Automatic Testing of Symbolic Execution Engines via Program Generation and Differential Testing. In ASE. IEEE Computer Society, 590--600."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"crossref","unstructured":"Gerwin Klein Kevin Elphinstone Gernot Heiser June Andronick David Cock Philip Derrin Dhammika Elkaduwe Kai Engelhardt Rafal Kolanski Michael Norrish Thomas Sewell Harvey Tuch and Simon Winwood. 2009. seL4: Formal Verification of an OS Kernel. In SOSP. ACM 207--220.","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"crossref","unstructured":"Christian Klinger Maria Christakis and Valentin W\u00fcstholz. 2019. Differentially Testing Soundness and Precision of Program Analyzers. In ISSTA. ACM 239--250.","DOI":"10.1145\/3293882.3330553"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"crossref","unstructured":"Muhammad Numair Mansur Maria Christakis and Valentin W\u00fcstholz. 2021. Metamorphic Testing of Datalog Engines. In ESEC\/FSE. ACM 639--650.","DOI":"10.1145\/3468264.3468573"},{"key":"e_1_3_2_1_31_1","unstructured":"Muhammad Numair Mansur Maria Christakis Valentin W\u00fcstholz and Fuyuan Zhang. 2020. Detecting Critical Bugs in SMT Solvers Using Blackbox Mutational Fuzzing. In ESEC\/FSE. ACM 701--712."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"crossref","unstructured":"Muhammad Numair Mansur Valentin W\u00fcstholz and Maria Christakis. 2023. Dependency-Aware Metamorphic Testing of Datalog Engines. In ISSTA. ACM 236--247.","DOI":"10.1145\/3597926.3598052"},{"key":"e_1_3_2_1_33_1","volume-title":"Verif. Reliab. 27","author":"Midtgaard Jan","year":"2017","unstructured":"Jan Midtgaard and Anders M\u00f8ller. 2017. QuickChecking Static Analysis Properties. Softw. Test., Verif. Reliab. 27 (2017). Issue 6."},{"key":"e_1_3_2_1_34_1","volume-title":"ECSTATIC: An Extensible Framework for Testing and Debugging Configurable Static Analysis","author":"Mordahl Austin","year":"2023","unstructured":"Austin Mordahl, Zenong Zhang, Dakota Soles, and Shiyi Wei. 2023. ECSTATIC: An Extensible Framework for Testing and Debugging Configurable Static Analysis. In ICSE. IEEE Computer Society, 550--562."},{"key":"e_1_3_2_1_35_1","first-page":"1","article-title":"Generative Type-Aware Mutation for Testing SMT Solvers","volume":"5","author":"Park Jiwon","year":"2021","unstructured":"Jiwon Park, Dominik Winterer, Chengyu Zhang, and Zhendong Su. 2021. Generative Type-Aware Mutation for Testing SMT Solvers. PACMPL 5 (2021), 1--19. Issue OOPSLA.","journal-title":"PACMPL"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2016.2532875"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32469-7_14"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_50"},{"key":"e_1_3_2_1_39_1","volume-title":"Feedback-Directed Metamorphic Testing. TOSEM 32","author":"Sun Chang-Ai","year":"2023","unstructured":"Chang-Ai Sun, Hepeng Dai, Huai Liu, and Tsong Yueh Chen. 2023. Feedback-Directed Metamorphic Testing. TOSEM 32 (2023), 20:1--20:34. Issue 1."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"crossref","unstructured":"Jubi Taneja Zhengyang Liu and John Regehr. 2020. Testing Static Analyses for Precision and Soundness. In CGO. ACM 81--93.","DOI":"10.1145\/3368826.3377927"},{"key":"e_1_3_2_1_41_1","volume-title":"On the Unusual Effectiveness of Type-Aware Operator Mutations for Testing SMT Solvers. PACMPL 4","author":"Winterer Dominik","year":"2020","unstructured":"Dominik Winterer, Chengyu Zhang, and Zhendong Su. 2020. On the Unusual Effectiveness of Type-Aware Operator Mutations for Testing SMT Solvers. PACMPL 4 (2020), 193:1--193:25. Issue OOPSLA."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"crossref","unstructured":"Dominik Winterer Chengyu Zhang and Zhendong Su. 2020. Validating SMT Solvers via Semantic Fusion. In PLDI. ACM 718--730.","DOI":"10.1145\/3385412.3385985"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"crossref","unstructured":"Xuejun Yang Yang Chen Eric Eide and John Regehr. 2011. Finding and Understanding Bugs in C Compilers. In PLDI. ACM 283--294.","DOI":"10.1145\/1993316.1993532"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"crossref","unstructured":"Chengyu Zhang Ting Su Yichen Yan Fuyuan Zhang Geguang Pu and Zhendong Su. 2019. Finding and Understanding Bugs in Software Model Checkers. In ESEC\/FSE. ACM 763--773.","DOI":"10.1145\/3338906.3338932"},{"key":"e_1_3_2_1_45_1","volume-title":"Statfier: Automated Testing of Static Analyzers via Semantic-Preserving Program Transformations. In ESEC\/FSE. ACM, 237--249.","author":"Zhang Huaien","year":"2023","unstructured":"Huaien Zhang, Yu Pei, Junjie Chen, and Shin Hwei Tan. 2023. Statfier: Automated Testing of Static Analyzers via Semantic-Preserving Program Transformations. In ESEC\/FSE. ACM, 237--249."},{"key":"e_1_3_2_1_46_1","volume-title":"Understanding and Detecting Annotation-Induced Faults of Static Analyzers. CoRR abs\/2402.14366","author":"Zhang Huaien","year":"2024","unstructured":"Huaien Zhang, Yu Pei, Shuyun Liang, and Shin Hwei Tan. 2024. Understanding and Detecting Annotation-Induced Faults of Static Analyzers. CoRR abs\/2402.14366 (2024)."}],"event":{"name":"ASE '24: 39th IEEE\/ACM International Conference on Automated Software Engineering","location":"Sacramento CA USA","acronym":"ASE '24","sponsor":["SIGAI ACM Special Interest Group on Artificial Intelligence","SIGSOFT ACM Special Interest Group on Software Engineering","IEEE CS"]},"container-title":["Proceedings of the 39th IEEE\/ACM International Conference on Automated Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3691620.3695034","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3691620.3695034","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T00:04:07Z","timestamp":1750291447000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3691620.3695034"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,27]]},"references-count":46,"alternative-id":["10.1145\/3691620.3695034","10.1145\/3691620"],"URL":"https:\/\/doi.org\/10.1145\/3691620.3695034","relation":{},"subject":[],"published":{"date-parts":[[2024,10,27]]},"assertion":[{"value":"2024-10-27","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}