{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,12]],"date-time":"2025-11-12T03:29:46Z","timestamp":1762918186626,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":37,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,11,16]],"date-time":"2020-11-16T00:00:00Z","timestamp":1605484800000},"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,11,16]]},"DOI":"10.1145\/3425898.3426959","type":"proceedings-article","created":{"date-parts":[[2020,11,25]],"date-time":"2020-11-25T01:26:21Z","timestamp":1606267581000},"page":"22-34","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Correctness-by-construction for feature-oriented software product lines"],"prefix":"10.1145","author":[{"given":"Tabea","family":"Bordis","sequence":"first","affiliation":[{"name":"TU Braunschweig, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tobias","family":"Runge","sequence":"additional","affiliation":[{"name":"TU Braunschweig, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ina","family":"Schaefer","sequence":"additional","affiliation":[{"name":"TU Braunschweig, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,11,16]]},"reference":[{"volume-title":"The B-Book: Assigning Programs to Meanings","author":"Abrial Jean-Raymond","key":"e_1_3_2_2_1_1","unstructured":"Jean-Raymond Abrial . 2005. The B-Book: Assigning Programs to Meanings . Cambridge University Press . Jean-Raymond Abrial. 2005. The B-Book: Assigning Programs to Meanings. Cambridge University Press."},{"key":"e_1_3_2_2_2_1","volume-title":"Modeling in Event-B: System and Software Engineering","author":"Abrial Jean-Raymond","unstructured":"Jean-Raymond Abrial . 2010. Modeling in Event-B: System and Software Engineering ( 1 st ed.). Jean-Raymond Abrial. 2010. Modeling in Event-B: System and Software Engineering (1st ed.).","edition":"1"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-010-0145-y"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"crossref","unstructured":"Wolfgang Ahrendt Bernhard Beckert Richard Bubel Reiner H\u00e4hnle Peter H. Schmitt and Mattias Ulbrich. 2016. Deductive Software Verification-The KeY Book.  Wolfgang Ahrendt Bernhard Beckert Richard Bubel Reiner H\u00e4hnle Peter H. Schmitt and Mattias Ulbrich. 2016. Deductive Software Verification-The KeY Book.","DOI":"10.1007\/978-3-319-49812-6"},{"key":"e_1_3_2_2_5_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_2_6_1","doi-asserted-by":"crossref","unstructured":"Sven Apel Alexander von Rhein Thomas Th\u00fcm and Christian K\u00e4stner. 2013. Feature-Interaction Detection Based on Feature-Based Specifications. 57 12 ( 2013 ) 2399-2409.  Sven Apel Alexander von Rhein Thomas Th\u00fcm and Christian K\u00e4stner. 2013. Feature-Interaction Detection Based on Feature-Based Specifications. 57 12 ( 2013 ) 2399-2409.","DOI":"10.1016\/j.comnet.2013.02.025"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"crossref","unstructured":"Ralph-Johan Back. 2009. Invariant Based Programming: Basic Approach and Teaching Experiences. Formal Aspects of Computing 21 3 ( 2009 ) 227-244.  Ralph-Johan Back. 2009. Invariant Based Programming: Basic Approach and Teaching Experiences. Formal Aspects of Computing 21 3 ( 2009 ) 227-244.","DOI":"10.1007\/s00165-008-0070-y"},{"key":"e_1_3_2_2_8_1","volume-title":"Testing and Verifying Invariant Based Programs in the SOCOS Environment. In International Conference on Tests and Proofs. Springer, 61-78","author":"Back Ralph-Johan","year":"2007","unstructured":"Ralph-Johan Back , Johannes Eriksson , and Magnus Myreen . 2007 . Testing and Verifying Invariant Based Programs in the SOCOS Environment. In International Conference on Tests and Proofs. Springer, 61-78 . Ralph-Johan Back, Johannes Eriksson, and Magnus Myreen. 2007. Testing and Verifying Invariant Based Programs in the SOCOS Environment. In International Conference on Tests and Proofs. Springer, 61-78."},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"crossref","unstructured":"Don Batory Jacob N. Sarvela and Axel Rauschmayer. 2004. Scaling Step-Wise Refinement. 30 6 ( 2004 ) 355-371.  Don Batory Jacob N. Sarvela and Axel Rauschmayer. 2004. Scaling Step-Wise Refinement. 30 6 ( 2004 ) 355-371.","DOI":"10.1109\/TSE.2004.23"},{"key":"e_1_3_2_2_10_1","volume-title":"Variational Correctness-by-Construction. In Proceedings of the 14th International Working Conference on Variability Modelling of Software-Intensive Systems. 1-9.","author":"Bordis Tabea","year":"2020","unstructured":"Tabea Bordis , Tobias Runge , Alexander Kn\u00fcppel , Thomas Th\u00fcm , and Ina Schaefer . 2020 . Variational Correctness-by-Construction. In Proceedings of the 14th International Working Conference on Variability Modelling of Software-Intensive Systems. 1-9. Tabea Bordis, Tobias Runge, Alexander Kn\u00fcppel, Thomas Th\u00fcm, and Ina Schaefer. 2020. Variational Correctness-by-Construction. In Proceedings of the 14th International Working Conference on Variability Modelling of Software-Intensive Systems. 1-9."},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"crossref","unstructured":"Daniel Bruns Vladimir Klebanov and Ina Schaefer. 2011. Verification of Software Product Lines with Delta-Oriented Slicing. 61-75.  Daniel Bruns Vladimir Klebanov and Ina Schaefer. 2011. Verification of Software Product Lines with Delta-Oriented Slicing. 61-75.","DOI":"10.1007\/978-3-642-18070-5_5"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78743-3_2"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"crossref","unstructured":"Andreas Classen Patrick Heymans Pierre-Yves Schobbens and Axel Legay. 2011. Symbolic Model Checking of Software Product Lines. 321-330.  Andreas Classen Patrick Heymans Pierre-Yves Schobbens and Axel Legay. 2011. Symbolic Model Checking of Software Product Lines. 321-330.","DOI":"10.1145\/1985793.1985838"},{"key":"e_1_3_2_2_14_1","unstructured":"Paul Clements and Linda Northrop. 2001. Software Product Lines: Practices and Patterns.  Paul Clements and Linda Northrop. 2001. Software Product Lines: Practices and Patterns."},{"key":"e_1_3_2_2_15_1","volume-title":"Implementing Tactics of Refinement in CRefine. In International Conference on Software Engineering and Formal Methods. Springer, 342-351","author":"Filho Madiel Conserva","year":"2012","unstructured":"Madiel Conserva Filho and Marcel Vinicius Medeiros Oliveira . 2012 . Implementing Tactics of Refinement in CRefine. In International Conference on Software Engineering and Formal Methods. Springer, 342-351 . Madiel Conserva Filho and Marcel Vinicius Medeiros Oliveira. 2012. Implementing Tactics of Refinement in CRefine. In International Conference on Software Engineering and Formal Methods. Springer, 342-351."},{"key":"e_1_3_2_2_16_1","unstructured":"Coq Development Team. 2010. The Coq Proof Assistant Reference Manual. LogiCal Project. Version 8.3.  Coq Development Team. 2010. The Coq Proof Assistant Reference Manual. LogiCal Project. Version 8.3."},{"key":"e_1_3_2_2_17_1","volume-title":"Generative Programming: Methods, Tools, and Applications.","author":"Czarnecki Krzysztof","year":"2000","unstructured":"Krzysztof Czarnecki and Ulrich Eisenecker . 2000 . Generative Programming: Methods, Tools, and Applications. Krzysztof Czarnecki and Ulrich Eisenecker. 2000. Generative Programming: Methods, Tools, and Applications."},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"crossref","unstructured":"Edsger W. Dijkstra. 1975. Guarded Commands Nondeterminacy and Formal Derivation of Programs. 18 8 ( 1975 ) 453-457.  Edsger W. Dijkstra. 1975. Guarded Commands Nondeterminacy and Formal Derivation of Programs. 18 8 ( 1975 ) 453-457.","DOI":"10.1145\/360933.360975"},{"key":"e_1_3_2_2_19_1","volume-title":"A Discipline of Programming","author":"Dijkstra Edsger W.","unstructured":"Edsger W. Dijkstra . 1976. A Discipline of Programming ( 1 st ed.). Prentice Hall PTR. Edsger W. Dijkstra. 1976. A Discipline of Programming (1st ed.). Prentice Hall PTR.","edition":"1"},{"key":"e_1_3_2_2_20_1","volume-title":"Roberto Erick Lopez-Herrejon, and Alexander Egyed","author":"Fischer Stefan","year":"2014","unstructured":"Stefan Fischer , Lukas Linsbauer , Roberto Erick Lopez-Herrejon, and Alexander Egyed . 2014 . Enhancing Clone-and-Own with Systematic Reuse for Developing Software Variants . 391-400. Stefan Fischer, Lukas Linsbauer, Roberto Erick Lopez-Herrejon, and Alexander Egyed. 2014. Enhancing Clone-and-Own with Systematic Reuse for Developing Software Variants. 391-400."},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"crossref","unstructured":"Rui C Gon\u00e7alves Don Batory Joao L Sobral and Taylor L Rich\u00e9. 2017. From Software Extensions to Product Lines of Dataflow Programs. Software & Systems Modeling 16 4 ( 2017 ) 929-947.  Rui C Gon\u00e7alves Don Batory Joao L Sobral and Taylor L Rich\u00e9. 2017. From Software Extensions to Product Lines of Dataflow Programs. Software & Systems Modeling 16 4 ( 2017 ) 929-947.","DOI":"10.1007\/s10270-015-0495-8"},{"key":"e_1_3_2_2_22_1","volume-title":"The Science of Programming","author":"Gries David","unstructured":"David Gries . 1981. The Science of Programming ( 1 st ed.). David Gries. 1981. The Science of Programming (1st ed.).","edition":"1"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"crossref","unstructured":"Reiner H\u00e4hnle and Ina Schaefer. 2012. A Liskov Principle for DeltaOriented Programming. 32-46.  Reiner H\u00e4hnle and Ina Schaefer. 2012. A Liskov Principle for DeltaOriented Programming. 32-46.","DOI":"10.1007\/978-3-642-34026-0_4"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"crossref","unstructured":"Christian K\u00e4stner and Sven Apel. 2008. Type-Checking Software Product Lines-A Formal Approach. 258-267.  Christian K\u00e4stner and Sven Apel. 2008. Type-Checking Software Product Lines-A Formal Approach. 258-267.","DOI":"10.1109\/ASE.2008.36"},{"key":"e_1_3_2_2_26_1","volume-title":"Watson","author":"Kourie Derrick G.","year":"2012","unstructured":"Derrick G. Kourie and Bruce W . Watson . 2012 . The Correctness-byConstruction Approach to Programming . Derrick G. Kourie and Bruce W. Watson. 2012. The Correctness-byConstruction Approach to Programming."},{"key":"e_1_3_2_2_27_1","volume-title":"Safety Analysis of Software Product Lines Using State-Based Modeling. 80, 11 ( 2007 )","author":"Liu Jing","year":"1879","unstructured":"Jing Liu , Josh Dehlinger , and Robyn Lutz . 2007. Safety Analysis of Software Product Lines Using State-Based Modeling. 80, 11 ( 2007 ) , 1879 -1892. Jing Liu, Josh Dehlinger, and Robyn Lutz. 2007. Safety Analysis of Software Product Lines Using State-Based Modeling. 80, 11 ( 2007 ), 1879-1892."},{"volume-title":"Programming from Specifications","author":"Morgan Carroll","key":"e_1_3_2_2_28_1","unstructured":"Carroll Morgan . 1998. Programming from Specifications . Prentice Hall . Carroll Morgan. 1998. Programming from Specifications. Prentice Hall."},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"crossref","unstructured":"Marcel Oliveira Ana Cavalcanti and Jim Woodcock. 2003. ArcAngel: A Tactic Language for Refinement. Formal Aspects of Computing 15 1 ( 2003 ) 28-47.  Marcel Oliveira Ana Cavalcanti and Jim Woodcock. 2003. ArcAngel: A Tactic Language for Refinement. Formal Aspects of Computing 15 1 ( 2003 ) 28-47.","DOI":"10.1007\/s00165-003-0003-8"},{"key":"e_1_3_2_2_30_1","volume-title":"CRefine: Support for the Circus Refinement Calculus. In 2008 Sixth IEEE International Conference on Software Engineering and Formal Methods. IEEE, 281-290","author":"Medeiros Oliveira Marcel Vinicius","year":"2008","unstructured":"Marcel Vinicius Medeiros Oliveira , Alessandro Cavalcante Gurgel , and CG Castro . 2008 . CRefine: Support for the Circus Refinement Calculus. In 2008 Sixth IEEE International Conference on Software Engineering and Formal Methods. IEEE, 281-290 . Marcel Vinicius Medeiros Oliveira, Alessandro Cavalcante Gurgel, and CG Castro. 2008. CRefine: Support for the Circus Refinement Calculus. In 2008 Sixth IEEE International Conference on Software Engineering and Formal Methods. IEEE, 281-290."},{"key":"e_1_3_2_2_32_1","volume-title":"van der Linden","author":"Pohl Klaus","year":"2005","unstructured":"Klaus Pohl , G\u00fcnter B\u00f6ckle , and Frank J . van der Linden . 2005 . Software Product Line Engineering: Foundations, Principles and Techniques . Klaus Pohl, G\u00fcnter B\u00f6ckle, and Frank J. van der Linden. 2005. Software Product Line Engineering: Foundations, Principles and Techniques."},{"key":"e_1_3_2_2_33_1","first-page":"347","article-title":"Configuration Lifting","author":"Post Hendrik","year":"2008","unstructured":"Hendrik Post and Carsten Sinz . 2008 . Configuration Lifting : Verification Meets Software Configuration. 347 - 350 . Hendrik Post and Carsten Sinz. 2008. Configuration Lifting: Verification Meets Software Configuration. 347-350.","journal-title":"Verification Meets Software Configuration."},{"key":"e_1_3_2_2_34_1","volume-title":"Watson","author":"Runge Tobias","year":"2019","unstructured":"Tobias Runge , Ina Schaefer , Loek Cleophas , Thomas Th\u00fcm , Derrick Kourie , and Bruce W . Watson . 2019 . Tool Support for Correctness-byConstruction . 25-42. Tobias Runge, Ina Schaefer, Loek Cleophas, Thomas Th\u00fcm, Derrick Kourie, and Bruce W. Watson. 2019. Tool Support for Correctness-byConstruction. 25-42."},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"crossref","unstructured":"Ina Schaefer Lorenzo Bettini Viviana Bono Ferruccio Damiani and Nico Tanzarella. 2010. Delta-Oriented Programming of Software Product Lines. 77-91.  Ina Schaefer Lorenzo Bettini Viviana Bono Ferruccio Damiani and Nico Tanzarella. 2010. Delta-Oriented Programming of Software Product Lines. 77-91.","DOI":"10.1007\/978-3-642-15579-6_6"},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"crossref","unstructured":"Thomas Th\u00fcm Sven Apel Christian K\u00e4stner Ina Schaefer and Gunter Saake. 2014. A Classification and Survey of Analysis Strategies for Software Product Lines. 47 1 ( 2014 ) 6 : 1-6 : 45.  Thomas Th\u00fcm Sven Apel Christian K\u00e4stner Ina Schaefer and Gunter Saake. 2014. A Classification and Survey of Analysis Strategies for Software Product Lines. 47 1 ( 2014 ) 6 : 1-6 : 45.","DOI":"10.1145\/2580950"},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"crossref","unstructured":"Thomas Th\u00fcm Christian K\u00e4stner Fabian Benduhn Jens Meinicke Gunter Saake and Thomas Leich. 2014. FeatureIDE: An Extensible Framework for Feature-Oriented Software Development. 79 0 ( 2014 ) 70-85.  Thomas Th\u00fcm Christian K\u00e4stner Fabian Benduhn Jens Meinicke Gunter Saake and Thomas Leich. 2014. FeatureIDE: An Extensible Framework for Feature-Oriented Software Development. 79 0 ( 2014 ) 70-85.","DOI":"10.1016\/j.scico.2012.06.002"},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"crossref","unstructured":"Thomas Th\u00fcm Alexander Kn\u00fcppel Stefan Kr\u00fcger Stefanie Bolle and Ina Schaefer. 2019. Feature-Oriented Contract Composition. 152 ( 2019 ) 83-107.  Thomas Th\u00fcm Alexander Kn\u00fcppel Stefan Kr\u00fcger Stefanie Bolle and Ina Schaefer. 2019. Feature-Oriented Contract Composition. 152 ( 2019 ) 83-107.","DOI":"10.1016\/j.jss.2019.01.044"},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"crossref","unstructured":"Thomas Th\u00fcm Ina Schaefer Martin Kuhlemann and Sven Apel. 2011. Proof Composition for Deductive Verification of Software Product Lines. 270-277.  Thomas Th\u00fcm Ina Schaefer Martin Kuhlemann and Sven Apel. 2011. Proof Composition for Deductive Verification of Software Product Lines. 270-277.","DOI":"10.1109\/ICSTW.2011.48"}],"event":{"name":"GPCE '20: Concepts and Experiences","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Virtual USA","acronym":"GPCE '20"},"container-title":["Proceedings of the 19th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3425898.3426959","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3425898.3426959","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:24:24Z","timestamp":1750195464000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3425898.3426959"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11,16]]},"references-count":37,"alternative-id":["10.1145\/3425898.3426959","10.1145\/3425898"],"URL":"https:\/\/doi.org\/10.1145\/3425898.3426959","relation":{},"subject":[],"published":{"date-parts":[[2020,11,16]]},"assertion":[{"value":"2020-11-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}