{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,12]],"date-time":"2025-12-12T13:35:46Z","timestamp":1765546546802,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":51,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,2,5]],"date-time":"2020-02-05T00:00:00Z","timestamp":1580860800000},"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":[[2020,2,5]]},"DOI":"10.1145\/3377024.3377036","type":"proceedings-article","created":{"date-parts":[[2020,2,6]],"date-time":"2020-02-06T17:20:12Z","timestamp":1581009612000},"page":"1-9","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":22,"title":["SMT-based variability analyses in FeatureIDE"],"prefix":"10.1145","author":[{"given":"Joshua","family":"Sprey","sequence":"first","affiliation":[{"name":"TU Braunschweig, Brunswick, Germany"}]},{"given":"Chico","family":"Sundermann","sequence":"additional","affiliation":[{"name":"TU Braunschweig, Brunswick, Germany"}]},{"given":"Sebastian","family":"Krieter","sequence":"additional","affiliation":[{"name":"Otto-von-Guericke-University, Magdeburg, Germany"}]},{"given":"Michael","family":"Nieke","sequence":"additional","affiliation":[{"name":"TU Braunschweig, Brunswick, Germany"}]},{"given":"Jacopo","family":"Mauro","sequence":"additional","affiliation":[{"name":"University of Southern Denmark, Odense, Denmark"}]},{"given":"Thomas","family":"Th\u00fcm","sequence":"additional","affiliation":[{"name":"University of Ulm, Germany"}]},{"given":"Ina","family":"Schaefer","sequence":"additional","affiliation":[{"name":"TU Braunschweig, Brunswick, Germany"}]}],"member":"320","published-online":{"date-parts":[[2020,2,6]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"crossref","unstructured":"Sven Apel Don Batory Christian K\u00e4stner and Gunter Saake. 2013. Feature-Oriented Software Product Lines.  Sven Apel Don Batory Christian K\u00e4stner and Gunter Saake. 2013. Feature-Oriented Software Product Lines.","DOI":"10.1007\/978-3-642-37521-7"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2015.7102591"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"crossref","unstructured":"Don Batory. 2005. Feature Models Grammars and Propositional Formulas. 7--20.  Don Batory. 2005. Feature Models Grammars and Propositional Formulas. 7--20.","DOI":"10.1007\/11554844_3"},{"key":"e_1_3_2_1_4_1","volume-title":"David Felipe Benavides Cuevas, and Antonio Ruiz Cort\u00e9s","author":"Batory Don","year":"2006","unstructured":"Don Batory , David Felipe Benavides Cuevas, and Antonio Ruiz Cort\u00e9s . 2006 . Automated analysis of feature models: challenges ahead. Communications of the ACM-Software product line, 49 (12), 45--47. (2006). Don Batory, David Felipe Benavides Cuevas, and Antonio Ruiz Cort\u00e9s. 2006. Automated analysis of feature models: challenges ahead. Communications of the ACM-Software product line, 49 (12), 45--47. (2006)."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"crossref","unstructured":"David Benavides Antonio Ruiz-Cort\u00e9s and Pablo Trinidad. 2005. Automated Reasoning on Feature Models. 491--503.  David Benavides Antonio Ruiz-Cort\u00e9s and Pablo Trinidad. 2005. Automated Reasoning on Feature Models. 491--503.","DOI":"10.1007\/11431855_34"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.is.2010.01.001"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2430502.2430513"},{"key":"e_1_3_2_1_8_1","volume-title":"d.]. SAT4J: A Satisfiability Library for Java. Website. Available online at http:\/\/www.sat4j.org\/","author":"Berre Daniel Le","year":"2010","unstructured":"Daniel Le Berre . [n. d.]. SAT4J: A Satisfiability Library for Java. Website. Available online at http:\/\/www.sat4j.org\/ ; visited on November 9th, 2010 . Daniel Le Berre. [n. d.]. SAT4J: A Satisfiability Library for Java. Website. Available online at http:\/\/www.sat4j.org\/; visited on November 9th, 2010."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"crossref","unstructured":"Paul Maximilian Bittner Thomas Th\u00fcm and Ina Schaefer. 2019. SAT Encodings of the At-Most-k Constraint - A Case Study on Configuring University Courses. To appear.  Paul Maximilian Bittner Thomas Th\u00fcm and Ina Schaefer. 2019. SAT Encodings of the At-Most-k Constraint - A Case Study on Configuring University Courses. To appear.","DOI":"10.1007\/978-3-030-30446-1_7"},{"key":"e_1_3_2_1_10_1","volume-title":"International Workshop on Software Product-Family Engineering. Springer, 13--21","author":"Bosch Jan","year":"2001","unstructured":"Jan Bosch , Gert Florijn , Danny Greefhorst , Juha Kuusela , J Henk Obbink , and Klaus Pohl . 2001 . Variability issues in software product lines . In International Workshop on Software Product-Family Engineering. Springer, 13--21 . Jan Bosch, Gert Florijn, Danny Greefhorst, Juha Kuusela, J Henk Obbink, and Klaus Pohl. 2001. Variability issues in software product lines. In International Workshop on Software Product-Family Engineering. Springer, 13--21."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31759-0_19"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2110147.2110167"},{"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\/1995376.1995394"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-015-0503-z"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814204.2814222"},{"key":"e_1_3_2_1_18_1","unstructured":"Richard Heijblom. 2013. Potential of Integer Programming for Optimization Analysis of Extended Feature Models. (2013).  Richard Heijblom. 2013. Potential of Integer Programming for Optimization Analysis of Extended Feature Models. (2013)."},{"key":"e_1_3_2_1_19_1","unstructured":"Mikolas Janota. 2008. Do SAT solvers make good configurators?. In SPLC (2). 191--195.  Mikolas Janota. 2008. Do SAT solvers make good configurators?. In SPLC (2) . 191--195."},{"key":"e_1_3_2_1_20_1","volume-title":"Antenna engineering handbook","author":"Johnson Richard C","year":"1984","unstructured":"Richard C Johnson and Henry Jasik . 1984. Antenna engineering handbook . New York , McGraw-Hill Book Company , 1984 , 1356 p. No individual items are abstracted in this volume. (1984). Richard C Johnson and Henry Jasik. 1984. Antenna engineering handbook. New York, McGraw-Hill Book Company, 1984, 1356 p. No individual items are abstracted in this volume. (1984)."},{"volume-title":"Detecting inadmissible and necessary variables in large propositional formulae","author":"Kaiser Andreas","key":"e_1_3_2_1_21_1","unstructured":"Andreas Kaiser and Wolfgang K\u00fcchlin . 2001. Detecting inadmissible and necessary variables in large propositional formulae . In University of Siena . Citeseer. Andreas Kaiser and Wolfgang K\u00fcchlin. 2001. Detecting inadmissible and necessary variables in large propositional formulae. In University of Siena. Citeseer."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/590631.590645"},{"key":"e_1_3_2_1_24_1","volume-title":"Feature-oriented product line engineering","author":"Kang Kyo C","year":"2002","unstructured":"Kyo C Kang , Jaejoon Lee , and Patrick Donohoe . 2002. Feature-oriented product line engineering . IEEE software 19, 4 ( 2002 ), 58--65. Kyo C Kang, Jaejoon Lee, and Patrick Donohoe. 2002. Feature-oriented product line engineering. IEEE software 19, 4 (2002), 58--65."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48869-1_11"},{"key":"e_1_3_2_1_26_1","unstructured":"Alexander Kn\u00fcppel Thomas Th\u00fcm Stephan Mennicke Jens Meinicke and Ina Schaefer. 2018. Is There a Mismatch between Real-World Feature Models and Product-Line Research? Matthias Tichy Eric Bodden Marco Kuhrmann Stefan Wagner and Jan-Philipp Stegh\u00f6fer (Eds.). 53--54. https:\/\/dl.gi.de\/20.500.12116\/16312  Alexander Kn\u00fcppel Thomas Th\u00fcm Stephan Mennicke Jens Meinicke and Ina Schaefer. 2018. Is There a Mismatch between Real-World Feature Models and Product-Line Research? Matthias Tichy Eric Bodden Marco Kuhrmann Stefan Wagner and Jan-Philipp Stegh\u00f6fer (Eds.). 53--54. https:\/\/dl.gi.de\/20.500.12116\/16312"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2993236.2993248"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180159"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1134285.1134303"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"crossref","unstructured":"Mike Mannion. 2002. Using First-Order Logic for Product Line Model Validation. 176--187.  Mike Mannion. 2002. Using First-Order Logic for Product Line Model Validation. 176--187.","DOI":"10.1007\/3-540-45652-X_11"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3109729.3109752"},{"key":"e_1_3_2_1_32_1","volume-title":"SMT Workshop 2012 10th International Workshop on Satisfiability Modulo Theories SMT-COMP. Citeseer, 107","author":"Michel Rapha\u00ebl","year":"2012","unstructured":"Rapha\u00ebl Michel , Arnaud Hubaux , Vijay Ganesh , and Patrick Heymans . 2012 . An SMT-based approach to automated configuration . In SMT Workshop 2012 10th International Workshop on Satisfiability Modulo Theories SMT-COMP. Citeseer, 107 . Rapha\u00ebl Michel, Arnaud Hubaux, Vijay Ganesh, and Patrick Heymans. 2012. An SMT-based approach to automated configuration. In SMT Workshop 2012 10th International Workshop on Satisfiability Modulo Theories SMT-COMP. Citeseer, 107."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3238201"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3278122.3278123"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2866614.2866625"},{"key":"e_1_3_2_1_36_1","unstructured":"Linda Northrop and P. Clements. 2007. A Framework for Software Product Line Practice Version 5.0. SEI (2007).  Linda Northrop and P. Clements. 2007. A Framework for Software Product Line Practice Version 5.0. SEI (2007)."},{"key":"e_1_3_2_1_37_1","volume-title":"Antenna: An Ant-to-End Solution For Wireless Java. Website. Available online at http:\/\/antenna.sourceforge.net\/","author":"Pleumann J\u00f6rg","year":"2011","unstructured":"J\u00f6rg Pleumann , Omry Yadan , and Erik Wetterberg . 2011 . Antenna: An Ant-to-End Solution For Wireless Java. Website. Available online at http:\/\/antenna.sourceforge.net\/ ; visited on November 22nd, 2011. J\u00f6rg Pleumann, Omry Yadan, and Erik Wetterberg. 2011. Antenna: An Ant-to-End Solution For Wireless Java. Website. Available online at http:\/\/antenna.sourceforge.net\/; visited on November 22nd, 2011."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2003.04.002"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2884781.2884823"},{"key":"e_1_3_2_1_40_1","unstructured":"Sergio Segura. 2008. Automated Analysis of Feature Models Using Atomic Sets.. In SPLC (2). 201--207.  Sergio Segura. 2008. Automated Analysis of Feature Models Using Atomic Sets.. In SPLC (2) . 201--207."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1868294.1868300"},{"key":"e_1_3_2_1_42_1","unstructured":"Joshua Sprey and Chico Sundermann. 2018. Computing Attribute Ranges for Partial Configurations with JavaSMT. (2018).  Joshua Sprey and Chico Sundermann. 2018. Computing Attribute Ranges for Partial Configurations with JavaSMT. (2018)."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3377024.3377025"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1966445.1966451"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2580950"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2009.5070526"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2012.06.002"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/SPLC.2011.53"},{"key":"e_1_3_2_1_49_1","volume-title":"workshop on software variability management for product derivation-towards tool support","volume":"44","author":"von der Ma\u00dfen Thomas","year":"2004","unstructured":"Thomas von der Ma\u00dfen and Horst Lichter . 2004 . Deficiencies in feature models . In workshop on software variability management for product derivation-towards tool support , Vol. 44 . 21. Thomas von der Ma\u00dfen and Horst Lichter. 2004. Deficiencies in feature models. In workshop on software variability management for product derivation-towards tool support, Vol. 44. 21."},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49665-7_10"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.5555\/2337223.2337231"},{"key":"e_1_3_2_1_52_1","volume-title":"A Propositional Logic-Based Method for Verification of Feature Models. Formal Methods and Software Engineering","author":"Zhang Wei","year":"2004","unstructured":"Wei Zhang , Haiyan Zhao , and Hong Mei . 2004. A Propositional Logic-Based Method for Verification of Feature Models. Formal Methods and Software Engineering ( 2004 ), 115--130. Wei Zhang, Haiyan Zhao, and Hong Mei. 2004. A Propositional Logic-Based Method for Verification of Feature Models. Formal Methods and Software Engineering (2004), 115--130."},{"key":"e_1_3_2_1_53_1","volume-title":"Available online at http:\/\/www.kernel.org\/doc\/Documentation\/kbuild\/kconfig-language.txt","author":"Zippel Roman","year":"2017","unstructured":"Roman Zippel . 2017. K Config Documentation . Website. Available online at http:\/\/www.kernel.org\/doc\/Documentation\/kbuild\/kconfig-language.txt ; visited on May 10th, 2017 . Roman Zippel. 2017. KConfig Documentation. Website. Available online at http:\/\/www.kernel.org\/doc\/Documentation\/kbuild\/kconfig-language.txt; visited on May 10th, 2017."}],"event":{"name":"VaMoS '20: 14th International Working Conference on Variability Modelling of Software-Intensive Systems","acronym":"VaMoS '20","location":"Magdeburg Germany"},"container-title":["Proceedings of the 14th International Working Conference on Variability Modelling of Software-Intensive Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3377024.3377036","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3377024.3377036","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:23:49Z","timestamp":1750202629000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3377024.3377036"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,2,5]]},"references-count":51,"alternative-id":["10.1145\/3377024.3377036","10.1145\/3377024"],"URL":"https:\/\/doi.org\/10.1145\/3377024.3377036","relation":{},"subject":[],"published":{"date-parts":[[2020,2,5]]},"assertion":[{"value":"2020-02-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}