{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:45:09Z","timestamp":1780994709125,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":42,"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.3695035","type":"proceedings-article","created":{"date-parts":[[2024,10,18]],"date-time":"2024-10-18T15:39:19Z","timestamp":1729265959000},"page":"344-355","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Constraint-Based Test Oracles for Program Analyzers"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-7072-8908","authenticated-orcid":false,"given":"Markus","family":"Fleischmann","sequence":"first","affiliation":[{"name":"TU Wien, Vienna, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-4137-5163","authenticated-orcid":false,"given":"David","family":"Kaindlstorfer","sequence":"additional","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.]. The International Satisfiability Modulo Theories Competition. https:\/\/smt-comp.github.io."},{"key":"e_1_3_2_1_2_1","unstructured":"Lukas Atkinson and Michael F\u00f6rderer. [n.d.]. gcovr. https:\/\/gcovr.com\/en\/stable."},{"key":"e_1_3_2_1_3_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_4_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_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48288-9_9"},{"key":"e_1_3_2_1_6_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_7_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_8_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_9_1","doi-asserted-by":"crossref","unstructured":"Maria Christakis Peter M\u00fcller and Valentin W\u00fcstholz. 2016. Guiding Dynamic Symbolic Execution Toward Unverified Program Executions. In ICSE. ACM 144--155.","DOI":"10.1145\/2884781.2884843"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"e_1_3_2_1_11_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_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28891-3_12"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_14_1","volume-title":"TACAS (LNCS","volume":"423","author":"Ermis Evren","year":"2014","unstructured":"Evren Ermis, Alexander Nutz, Daniel Dietsch, Jochen Hoenicke, and Andreas Podelski. 2014. Ultimate Kojak - (Competition Contribution). In TACAS (LNCS, Vol. 8413). Springer, 421--423."},{"key":"e_1_3_2_1_15_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_16_1","doi-asserted-by":"crossref","unstructured":"Azadeh Farzan Dominik Klumpp and Andreas Podelski. 2022. Sound Sequentialization for Concurrent Program Verification. In PLDI. ACM 506--521.","DOI":"10.1145\/3519939.3523727"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66706-5_7"},{"key":"e_1_3_2_1_18_1","volume-title":"Navas","author":"Gurfinkel Arie","year":"2015","unstructured":"Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, and Jorge A. Navas. 2015. The SeaHorn Verification Framework. In CAV (LNCS, Vol. 9206). Springer, 343--361."},{"key":"e_1_3_2_1_19_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_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03237-0_7"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_2"},{"key":"e_1_3_2_1_22_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_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_52"},{"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":"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_27_1","first-page":"1","article-title":"Fuzzle: Making a Puzzle for Fuzzers","volume":"45","author":"Lee Haeun","year":"2022","unstructured":"Haeun Lee, Soomin Kim, and Sang Kil Cha. 2022. Fuzzle: Making a Puzzle for Fuzzers. In ASE. ACM, 45:1--45:12.","journal-title":"ASE. ACM"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_2_1_29_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_30_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_31_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_32_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_33_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_34_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_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32469-7_14"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_50"},{"key":"e_1_3_2_1_37_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_38_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_39_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_40_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_41_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_42_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."}],"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.3695035","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3691620.3695035","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.3695035"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,27]]},"references-count":42,"alternative-id":["10.1145\/3691620.3695035","10.1145\/3691620"],"URL":"https:\/\/doi.org\/10.1145\/3691620.3695035","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"}}]}}