{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,16]],"date-time":"2026-10-16T21:06:38Z","timestamp":1792184798202,"version":"4.4.0"},"publisher-location":"New York, NY, USA","reference-count":46,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,2,7]],"date-time":"2024-02-07T00:00:00Z","timestamp":1707264000000},"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":[[2024,2,7]]},"DOI":"10.1145\/3634713.3634714","type":"proceedings-article","created":{"date-parts":[[2024,1,23]],"date-time":"2024-01-23T18:06:19Z","timestamp":1706033179000},"page":"17-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Partial Proofs to Optimize Deductive Verification of Feature-Oriented Software Product Lines"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-9022-859X","authenticated-orcid":false,"given":"Maximilian","family":"Kodetzki","sequence":"first","affiliation":[{"name":"Karlsruhe Institute of Technology, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-2886-0862","authenticated-orcid":false,"given":"Tabea","family":"Bordis","sequence":"additional","affiliation":[{"name":"Karlsruhe Institute of Technology, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9154-7743","authenticated-orcid":false,"given":"Tobias","family":"Runge","sequence":"additional","affiliation":[{"name":"Karlsruhe Institute of Technology, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7153-761X","authenticated-orcid":false,"given":"Ina","family":"Schaefer","sequence":"additional","affiliation":[{"name":"Karlsruhe Institute of Technology, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,2,7]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-49812-6"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37521-7"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.comnet.2013.02.025"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-019-00501-3"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2003.1201271"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2004.1347505"},{"key":"e_1_3_2_1_7_1","unstructured":"[7] Fabian Benduhn. 2012. Contract-Aware Feature Composition. Bachelor\u2019s Thesis."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2013.07.016"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-26236-4_13"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.cola.2022.101119"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18070-5_5"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-46508-1_8"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","unstructured":"Yoonsik Cheon. 2003. A runtime assertion checker for the Java Modeling Language. https:\/\/doi.org\/10.31274\/rtd-180813-9872","DOI":"10.31274\/rtd-180813-9872"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-013-0278-3"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-011-0211-0"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","unstructured":"Alexander Gruler Martin Leucker and Kathrin Scheidemann. 2008. Modeling and Model Checking Software Product Lines. In Formal methods for open object-based distributed systems. Vol.\u00a05051. 113\u2013131. https:\/\/doi.org\/10.1007\/978-3-540-68863-1_8","DOI":"10.1007\/978-3-540-68863-1_8"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","unstructured":"Rainer H\u00e4hnle and Marieke Huisman. 2017. 24 Challenges in Deductive Software Verification. In ARCADE. 1st International Workshop on Automated Reasoning: Challenges Applications Directions Exemplary Achievements(EPiC Series in Computing Vol.\u00a051). EasyChair 37\u201341. https:\/\/doi.org\/10.29007\/j2cm","DOI":"10.29007\/j2cm"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-91908-9_18"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"crossref","unstructured":"Kyo Kang Sholom Cohen James Hess William Novak and A.\u00a0Spencer Peterson. 1990. Feature-Oriented Domain Analysis (FODA) Feasibility Study.","DOI":"10.21236\/ADA235785"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2211616.2211617"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69061-0_13"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-64354-6_5"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27919-5"},{"key":"e_1_3_2_1_25_1","volume-title":"Proof Repositories for Correct-by-Construction Software Product Lines. Master\u2019s Thesis","author":"Kuiter Elias","unstructured":"Elias Kuiter. 2020. Proof Repositories for Correct-by-Construction Software Product Lines. Master\u2019s Thesis. Otto-von-Guericke University Magdeburg, Magdeburg."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3510466.3511272"},{"key":"e_1_3_2_1_27_1","volume-title":"Leavens and Cheon Yoonsik","author":"T.","year":"2006","unstructured":"Gary\u00a0T. Leavens and Cheon Yoonsik. 2006. Design by Contract with JML."},{"key":"e_1_3_2_1_28_1","unstructured":"S.\u00a0D. Litvintchouk and V.\u00a0R. Pratt. 1977. A Proof-Checker for Dynamic Logic."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2007.01.047"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-61443-4"},{"key":"e_1_3_2_1_31_1","unstructured":"[31] Maria Pelevina. 2015. Realization and Extension of Abstract Operation Contracts for Program Logic. Bachelor\u2019s Thesis."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(00)00018-6"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-28901-1"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0053389"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-16722-6_2"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15579-6_6"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45070-2_12"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2019136.2019144"},{"key":"e_1_3_2_1_39_1","unstructured":"[39] Thomas Th\u00fcm. 2015. Product-Line Specification and Verification with Feature-Oriented Contracts. Dissertation."},{"key":"e_1_3_2_1_40_1","unstructured":"Thomas Th\u00fcm Sven Apel Christian K\u00e4stner Martin Kuhlemann Ina Schaefer and Gunter Saake. 2012. Analysis Strategies for Software Product Lines."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2580950"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2019.01.044"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2371401.2371404"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSTW.2011.48"},{"key":"e_1_3_2_1_45_1","first-page":"67","article-title":"Checking a large routine. In Report of a Conference on High Speed Automatic Calculating machines","author":"Turing Alan","year":"1949","unstructured":"Alan Turing. 1949. Checking a large routine. In Report of a Conference on High Speed Automatic Calculating machines. Mathematical Laboratory, Cambridge, 67\u201369.","journal-title":"Mathematical Laboratory, Cambridge"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","unstructured":"Dries Vanoverberghe Nikolaj Bj\u00f8rner Jonathan de Halleux Wolfram Schulte and Nikolai Tillmann. 2008. Using Dynamic Symbolic Execution to Improve Deductive Verification. In Model checking software. Vol.\u00a05156. 9\u201325. https:\/\/doi.org\/10.1007\/978-3-540-85114-1_4","DOI":"10.1007\/978-3-540-85114-1_4"}],"event":{"name":"VaMoS 2024: 18th International Working Conference on Variability Modelling of Software-Intensive Systems","location":"Bern Switzerland","acronym":"VaMoS 2024"},"container-title":["Proceedings of the 18th International Working Conference on Variability Modelling of Software-Intensive Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3634713.3634714","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3634713.3634714","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,23]],"date-time":"2025-08-23T01:43:05Z","timestamp":1755913385000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3634713.3634714"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,2,7]]},"references-count":46,"alternative-id":["10.1145\/3634713.3634714","10.1145\/3634713"],"URL":"https:\/\/doi.org\/10.1145\/3634713.3634714","relation":{},"subject":[],"published":{"date-parts":[[2024,2,7]]},"assertion":[{"value":"2024-02-07","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}