{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,2]],"date-time":"2025-12-02T15:04:31Z","timestamp":1764687871196,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":29,"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.3377038","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":7,"title":["Variational correctness-by-construction"],"prefix":"10.1145","author":[{"given":"Tabea","family":"Bordis","sequence":"first","affiliation":[{"name":"TU Braunschweig, Braunschweig, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tobias","family":"Runge","sequence":"additional","affiliation":[{"name":"TU Braunschweig, Braunschweig, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander","family":"Kn\u00fcppel","sequence":"additional","affiliation":[{"name":"TU Braunschweig, Braunschweig, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Th\u00fcm","sequence":"additional","affiliation":[{"name":"University of Ulm, Ulm, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ina","family":"Schaefer","sequence":"additional","affiliation":[{"name":"TU Braunschweig, Braunschweig, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,2,6]]},"reference":[{"volume-title":"The B-Book: Assigning Programs to Meanings","author":"Abrial Jean-Raymond","key":"e_1_3_2_1_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_1_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_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-010-0145-y"},{"key":"e_1_3_2_1_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_1_5_1","volume-title":"Implementing Product Line Variabilities. 26, 3","author":"Anastasopoules Michalis","year":"2001","unstructured":"Michalis Anastasopoules and Critina Gacek . 2001. Implementing Product Line Variabilities. 26, 3 ( 2001 ), 109--117. Michalis Anastasopoules and Critina Gacek. 2001. Implementing Product Line Variabilities. 26, 3 (2001), 109--117."},{"key":"e_1_3_2_1_6_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_7_1","volume-title":"Scaling Step-Wise Refinement. 30, 6","author":"Batory Don","year":"2004","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."},{"key":"e_1_3_2_1_8_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_1_9_1","volume-title":"An Overview of Dynamic Software Product Line Architectures and Techniques: Observations from Research and Industry. 91","author":"Capilla Rafael","year":"2014","unstructured":"Rafael Capilla , Jan Bosch , Pablo Trinidad , Antonio Ruiz-Cort\u00e9s , and Mike Hinchey . 2014. An Overview of Dynamic Software Product Line Architectures and Techniques: Observations from Research and Industry. 91 ( 2014 ), 3--23. Rafael Capilla, Jan Bosch, Pablo Trinidad, Antonio Ruiz-Cort\u00e9s, and Mike Hinchey. 2014. An Overview of Dynamic Software Product Line Architectures and Techniques: Observations from Research and Industry. 91 (2014), 3--23."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"crossref","unstructured":"David R. Cok. 2011. OpenJML: JML for Java 7 by Extending OpenJDK. 472--479.  David R. Cok. 2011. OpenJML: JML for Java 7 by Extending OpenJDK. 472--479.","DOI":"10.1007\/978-3-642-20398-5_35"},{"key":"e_1_3_2_1_11_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_1_12_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_1_13_1","first-page":"453","article-title":"Guarded Commands","volume":"18","author":"Dijkstra Edsger W.","year":"1975","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.","journal-title":"Nondeterminacy and Formal Derivation of Programs."},{"key":"e_1_3_2_1_14_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_1_15_1","doi-asserted-by":"crossref","unstructured":"Yael Dubinsky Julia Rubin Thorsten Berger Slawomir Duszynski Martin Becker and Krzysztof Czarnecki. 2013. An Exploratory Study of Cloning in Industrial Software Product Lines. 25--34.  Yael Dubinsky Julia Rubin Thorsten Berger Slawomir Duszynski Martin Becker and Krzysztof Czarnecki. 2013. An Exploratory Study of Cloning in Industrial Software Product Lines. 25--34.","DOI":"10.1109\/CSMR.2013.13"},{"key":"e_1_3_2_1_16_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_1_17_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_1_18_1","doi-asserted-by":"crossref","unstructured":"Reiner H\u00e4hnle and Ina Schaefer. 2012. A Liskov Principle for Delta-Oriented Programming. 32--46.  Reiner H\u00e4hnle and Ina Schaefer. 2012. A Liskov Principle for Delta-Oriented Programming. 32--46.","DOI":"10.1007\/978-3-642-34026-0_4"},{"key":"e_1_3_2_1_19_1","volume-title":"Watson","author":"Kourie Derrick G.","year":"2012","unstructured":"Derrick G. Kourie and Bruce W . Watson . 2012 . The Correctness-by-Construction Approach to Programming . Derrick G. Kourie and Bruce W. Watson. 2012. The Correctness-by-Construction Approach to Programming."},{"key":"e_1_3_2_1_20_1","unstructured":"R. Kramer. 1998. iContract - The Java(Tm) Design by Contract(Tm) Tool. 295--307.  R. Kramer. 1998. iContract - The Java(Tm) Design by Contract(Tm) Tool. 295--307."},{"key":"e_1_3_2_1_21_1","volume-title":"Safety Analysis of Software Product Lines Using State-Based Modeling. 80, 11","author":"Liu Jing","year":"2007","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."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-003-0003-8"},{"key":"e_1_3_2_1_23_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_1_24_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-by-Construction . 25--42. Tobias Runge, Ina Schaefer, Loek Cleophas, Thomas Th\u00fcm, Derrick Kourie, and Bruce W. Watson. 2019. Tool Support for Correctness-by-Construction. 25--42."},{"key":"e_1_3_2_1_25_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_1_26_1","first-page":"1","article-title":"Automatic Detection of Feature Interactions Using the Java Modeling Language","volume":"7","author":"Scholz Wolfgang","year":"2011","unstructured":"Wolfgang Scholz , Thomas Th\u00fcm , Sven Apel , and Christian Lengauer . 2011 . Automatic Detection of Feature Interactions Using the Java Modeling Language : An Experience Report. Article 7 , 7: 1 -- 7 :8 pages. Wolfgang Scholz, Thomas Th\u00fcm, Sven Apel, and Christian Lengauer. 2011. Automatic Detection of Feature Interactions Using the Java Modeling Language: An Experience Report. Article 7, 7:1--7:8 pages.","journal-title":"An Experience Report. Article"},{"key":"e_1_3_2_1_27_1","volume-title":"Feature-Oriented Contract Composition. 152","author":"Th\u00fcm Thomas","year":"2019","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."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"crossref","unstructured":"Thomas Th\u00fcm Jens Meinicke Fabian Benduhn Martin Hentschel Alexander von Rhein and Gunter Saake. 2014. Potential Synergies of Theorem Proving and Model Checking for Software Product Lines. 177--186.  Thomas Th\u00fcm Jens Meinicke Fabian Benduhn Martin Hentschel Alexander von Rhein and Gunter Saake. 2014. Potential Synergies of Theorem Proving and Model Checking for Software Product Lines. 177--186.","DOI":"10.1145\/2648511.2648530"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-47166-2_52"}],"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.3377038","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3377024.3377038","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.3377038"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,2,5]]},"references-count":29,"alternative-id":["10.1145\/3377024.3377038","10.1145\/3377024"],"URL":"https:\/\/doi.org\/10.1145\/3377024.3377038","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"}}]}}