{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,16]],"date-time":"2026-10-16T21:07:10Z","timestamp":1792184830294,"version":"4.4.0"},"publisher-location":"New York, NY, USA","reference-count":61,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,8,18]],"date-time":"2021-08-18T00:00:00Z","timestamp":1629244800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1941816 and CCF-1840934"],"award-info":[{"award-number":["CCF-1941816 and CCF-1840934"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,8,20]]},"DOI":"10.1145\/3468264.3468578","type":"proceedings-article","created":{"date-parts":[[2021,10,29]],"date-time":"2021-10-29T14:11:43Z","timestamp":1635516703000},"page":"893-905","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":21,"title":["Finding broken Linux configuration specifications by statically analyzing the Kconfig language"],"prefix":"10.1145","author":[{"given":"Jeho","family":"Oh","sequence":"first","affiliation":[{"name":"University of Texas at Austin, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Necip Faz\u0131l","family":"Y\u0131ld\u0131ran","sequence":"additional","affiliation":[{"name":"University of Central Florida, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Julian","family":"Braha","sequence":"additional","affiliation":[{"name":"University of Central Florida, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1425-8873","authenticated-orcid":false,"given":"Paul","family":"Gazzillo","sequence":"additional","affiliation":[{"name":"University of Central Florida, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,8,18]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"2008. Boogie: An Intermediate Verification Language. https:\/\/www.microsoft.com\/en-us\/research\/project\/boogie-an-intermediate-verification-language\/  2008. Boogie: An Intermediate Verification Language. https:\/\/www.microsoft.com\/en-us\/research\/project\/boogie-an-intermediate-verification-language\/"},{"key":"e_1_3_2_1_2_1","unstructured":"2020. Kconfig macro language. https:\/\/www.kernel.org\/doc\/html\/latest\/kbuild\/kconfig-macro-language.html  2020. Kconfig macro language. https:\/\/www.kernel.org\/doc\/html\/latest\/kbuild\/kconfig-macro-language.html"},{"key":"e_1_3_2_1_3_1","unstructured":"2020. Kernel.org Bugzilla page. https:\/\/bugzilla.kernel.org\/  2020. Kernel.org Bugzilla page. https:\/\/bugzilla.kernel.org\/"},{"key":"e_1_3_2_1_4_1","unstructured":"2020. Undertaker Project Page. https:\/\/vamos.informatik.uni-erlangen.de\/trac\/undertaker  2020. Undertaker Project Page. https:\/\/vamos.informatik.uni-erlangen.de\/trac\/undertaker"},{"key":"e_1_3_2_1_5_1","unstructured":"2021. 0-Day Test Service. https:\/\/01.org\/lkp\/documentation\/0-day-test-service  2021. 0-Day Test Service. https:\/\/01.org\/lkp\/documentation\/0-day-test-service"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2642937.2642990"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3149119"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10922-015-9351-y"},{"key":"e_1_3_2_1_9_1","volume-title":"Proceedings of the 8th International Workshop on Satisfiability Modulo Theories","author":"Barrett Clark","year":"2010","unstructured":"Clark Barrett , Aaron Stump , and Cesare Tinelli . 2010 . The SMT-LIB Standard: Version 2.0 . In Proceedings of the 8th International Workshop on Satisfiability Modulo Theories ( Edinburgh, UK), A. Gupta and D. Kroening (Eds.). Clark Barrett, Aaron Stump, and Cesare Tinelli. 2010. The SMT-LIB Standard: Version 2.0. In Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, UK), A. Gupta and D. Kroening (Eds.)."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2013.34"},{"key":"e_1_3_2_1_11_1","volume-title":"SPLLIFT: Statically Analyzing Software Product Lines in Minutes Instead of Years. 355?364. isbn:9781450320146 https:\/\/doi.org\/10.1145\/2491956.2491976","author":"Bodden Eric","year":"2013","unstructured":"Eric Bodden , T\u00e1rsis Tol\u00eado , M\u00e1rcio Ribeiro , Claus Brabrand , Paulo Borba , and Mira Mezini . 2013 . SPLLIFT: Statically Analyzing Software Product Lines in Minutes Instead of Years. 355?364. isbn:9781450320146 https:\/\/doi.org\/10.1145\/2491956.2491976 Eric Bodden, T\u00e1rsis Tol\u00eado, M\u00e1rcio Ribeiro, Claus Brabrand, Paulo Borba, and Mira Mezini. 2013. SPLLIFT: Statically Analyzing Software Product Lines in Minutes Instead of Years. 355?364. isbn:9781450320146 https:\/\/doi.org\/10.1145\/2491956.2491976"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3368089.3409728"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2362536.2362544"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814204.2814222"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3336294.3336313"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2934466.2934467"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"crossref","unstructured":"Alejandra Garrido and Ralph Johnson. 2005. Analyzing Multiple Configurations of a C Program. In ICSM. 379\u2013388.  Alejandra Garrido and Ralph Johnson. 2005. Analyzing Multiple Configurations of a C Program. In ICSM. 379\u2013388.","DOI":"10.1109\/ICSM.2005.23"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106283"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254103"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984000"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2019.00047"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2019.00052"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"crossref","unstructured":"Alexandru Florin Iosif-Lazar Jean Melo Aleksandar S. Dimovski Claus Brabrand and Andrzej Wasowski. 2017. Effective Analysis of C Programs by Rewriting Variability. CoRR.  Alexandru Florin Iosif-Lazar Jean Melo Aleksandar S. Dimovski Claus Brabrand and Andrzej Wasowski. 2017. Effective Analysis of C Programs by Rewriting Variability. CoRR.","DOI":"10.22152\/programming-journal.org\/2017\/1\/1"},{"key":"e_1_3_2_1_25_1","unstructured":"Christian K\u00e4stner. 2020. kconfigreader. https:\/\/github.com\/ckaestne\/kconfigreader  Christian K\u00e4stner. 2020. kconfigreader. https:\/\/github.com\/ckaestne\/kconfigreader"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2048066.2048128"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384673"},{"key":"e_1_3_2_1_28_1","unstructured":"The kernel development community. 2020. Kconfig Language. https:\/\/www.kernel.org\/doc\/html\/latest\/kbuild\/kconfig-language.html  The kernel development community. 2020. Kconfig Language. https:\/\/www.kernel.org\/doc\/html\/latest\/kbuild\/kconfig-language.html"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1960275.1960284"},{"key":"e_1_3_2_1_30_1","unstructured":"Christian K\u00e4stner. 2017. Differential Testing for Variational Analyses: Experience from Developing KConfigReader. arxiv:1706.09357.  Christian K\u00e4stner. 2017. Differential Testing for Variational Analyses: Experience from Developing KConfigReader. arxiv:1706.09357."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491437"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2884781.2884793"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2866614.2866615"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3338906.3338967"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3168365.3168382"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2015.2415793"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSMR.2012.21"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.4885001"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.4563310"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.4950763"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908083"},{"key":"e_1_3_2_1_42_1","unstructured":"Steven She. 2013. LVAT Archive. https:\/\/code.google.com\/archive\/p\/linux-variability-analysis-tools\/  Steven She. 2013. LVAT Archive. https:\/\/code.google.com\/archive\/p\/linux-variability-analysis-tools\/"},{"key":"e_1_3_2_1_43_1","volume-title":"Formal semantics of the Kconfig language. Technical note","author":"She Steven","year":"2010","unstructured":"Steven She and Thorsten Berger . 2010. Formal semantics of the Kconfig language. Technical note , University of Waterloo , 24 ( 2010 ). Steven She and Thorsten Berger. 2010. Formal semantics of the Kconfig language. Technical note, University of Waterloo, 24 (2010)."},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985856"},{"key":"e_1_3_2_1_45_1","unstructured":"She Steven. 2013.\n  Feature Model Synthesis\n  . Ph.D. Dissertation. http:\/\/hdl.handle.net\/10012\/7834  She Steven. 2013. Feature Model Synthesis. Ph.D. Dissertation. http:\/\/hdl.handle.net\/10012\/7834"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28872-2_19"},{"key":"e_1_3_2_1_47_1","volume-title":"Proceedings of the International Workshop on Open Source Software and Product Lines (SPLC-OSSPL). 134\u2013140","author":"Sincero J.","unstructured":"J. Sincero , H. Schirmeier , W. Schr\u00f6der-Preikschat , and O. Spinczyk . 2007. Is the linux kernel a software product line? In Proceedings of the International Workshop on Open Source Software and Product Lines (SPLC-OSSPL). 134\u2013140 . J. Sincero, H. Schirmeier, W. Schr\u00f6der-Preikschat, and O. Spinczyk. 2007. Is the linux kernel a software product line? In Proceedings of the International Workshop on Open Source Software and Product Lines (SPLC-OSSPL). 134\u2013140."},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/1868294.1868300"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3377811.3380384"},{"key":"e_1_3_2_1_50_1","unstructured":"Jasper Spaans. 2020. Linux Kernel Mailing List. https:\/\/lkml.org\/  Jasper Spaans. 2020. Linux Kernel Mailing List. https:\/\/lkml.org\/"},{"key":"e_1_3_2_1_51_1","volume-title":"Proceedings of the 2014 USENIX Conference on USENIX Annual Technical Conference (USENIX ATC\u201914)","author":"Tartler Reinhard","year":"2014","unstructured":"Reinhard Tartler , Christian Dietrich , Julio Sincero , Wolfgang Schr\u00f6der-Preikschat , and Daniel Lohmann . 2014 . Static Analysis of Variability in System Software: The 90,000 #ifdefs Issue . In Proceedings of the 2014 USENIX Conference on USENIX Annual Technical Conference (USENIX ATC\u201914) . USENIX Association, USA. 421\u2013432. isbn:978 1931971102 Reinhard Tartler, Christian Dietrich, Julio Sincero, Wolfgang Schr\u00f6der-Preikschat, and Daniel Lohmann. 2014. Static Analysis of Variability in System Software: The 90,000 #ifdefs Issue. In Proceedings of the 2014 USENIX Conference on USENIX Annual Technical Conference (USENIX ATC\u201914). USENIX Association, USA. 421\u2013432. isbn:9781931971102"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/1966445.1966451"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0225-2"},{"key":"e_1_3_2_1_54_1","unstructured":"Linux Tovalds. 2020. Linux Kconfig Source Code. https:\/\/github.com\/torvalds\/linux\/tree\/master\/scripts\/kconfig  Linux Tovalds. 2020. Linux Kconfig Source Code. https:\/\/github.com\/torvalds\/linux\/tree\/master\/scripts\/kconfig"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3233027.3233035"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3280986"},{"key":"e_1_3_2_1_57_1","volume-title":"Configuration Workshop. 131\u2013138","author":"Walch Martin","year":"2015","unstructured":"Martin Walch , Rouven Walter , and Wolfgang K\u00fcchlin . 2015 . Formal analysis of the Linux kernel configuration with SAT solving . In Configuration Workshop. 131\u2013138 . Martin Walch, Rouven Walter, and Wolfgang K\u00fcchlin. 2015. Formal analysis of the Linux kernel configuration with SAT solving. In Configuration Workshop. 131\u2013138."},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/2661136.2661143"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.5555\/3155562.3155641"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3324884.3416577"},{"key":"e_1_3_2_1_61_1","volume-title":"Proceedings of the 19th European Conference on Artificial Intelligence (ECAI 2010) Workshop on Configuration.","author":"Zengler Christoph","year":"2010","unstructured":"Christoph Zengler and Wolfgang K\u00fcchlin . 2010 . Encoding the Linux kernel configuration in propositional logic . In Proceedings of the 19th European Conference on Artificial Intelligence (ECAI 2010) Workshop on Configuration. 2010, 51\u201356. Christoph Zengler and Wolfgang K\u00fcchlin. 2010. Encoding the Linux kernel configuration in propositional logic. In Proceedings of the 19th European Conference on Artificial Intelligence (ECAI 2010) Workshop on Configuration. 2010, 51\u201356."}],"event":{"name":"ESEC\/FSE '21: 29th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering","location":"Athens Greece","acronym":"ESEC\/FSE '21","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3468264.3468578","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3468264.3468578","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3468264.3468578","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:24:51Z","timestamp":1750195491000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3468264.3468578"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8,18]]},"references-count":61,"alternative-id":["10.1145\/3468264.3468578","10.1145\/3468264"],"URL":"https:\/\/doi.org\/10.1145\/3468264.3468578","relation":{},"subject":[],"published":{"date-parts":[[2021,8,18]]},"assertion":[{"value":"2021-08-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}