{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,2]],"date-time":"2025-12-02T15:09:16Z","timestamp":1764688156024,"version":"build-2065373602"},"publisher-location":"New York, NY, USA","reference-count":87,"publisher":"ACM","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,10,9]]},"DOI":"10.1145\/3759429.3762623","type":"proceedings-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T18:37:09Z","timestamp":1760035029000},"page":"99-115","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["X-by-Construction: Towards Ensuring Non-functional Properties in by-Construction Engineering"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-9022-859X","authenticated-orcid":false,"given":"Maximilian","family":"Kodetzki","sequence":"first","affiliation":[{"name":"KIT, Karlsruhe, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-2886-0862","authenticated-orcid":false,"given":"Tabea","family":"Bordis","sequence":"additional","affiliation":[{"name":"KIT, Karlsruhe, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4242-2725","authenticated-orcid":false,"given":"Alex","family":"Potanin","sequence":"additional","affiliation":[{"name":"Australian National University, Canberra, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7153-761X","authenticated-orcid":false,"given":"Ina","family":"Schaefer","sequence":"additional","affiliation":[{"name":"KIT, Karlsruhe, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10557-4_44"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","unstructured":"Wolfgang Ahrendt Bernhard Beckert Richard Bubel Reiner H\u00e4hnle Peter H. Schmitt and Mattias Ulbrich (Eds.). 2016. Deductive Software Verification \u2013 The KeY Book (Lecture Notes in Computer Science Vol. 10001). Springer International Publishing Cham. isbn:978-3-319-49811-9 978-3-319-49812-6 https:\/\/doi.org\/10.1007\/978-3-319-49812-6 10.1007\/978-3-319-49812-6","DOI":"10.1007\/978-3-319-49812-6"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","unstructured":"E. Albert P. Arenas S. Genaim G. Puebla and D. Zanardini. 2007. Cost Analysis of Java Bytecode. In Programming Languages and Systems. Springer Berlin Heidelberg. 157\u2013172. isbn:978-3-540-71316-6 https:\/\/doi.org\/10.1007\/978-3-540-71316-6_12 10.1007\/978-3-540-71316-6_12","DOI":"10.1007\/978-3-540-71316-6_12"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","unstructured":"Ralph-Johan Back and Joakim Wright. 1998. Refinement Calculus. Springer. https:\/\/doi.org\/10.1007\/978-1-4612-1674-2 10.1007\/978-1-4612-1674-2","DOI":"10.1007\/978-1-4612-1674-2"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/183432.183527"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2808231"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/FPL53798.2021.00075"},{"key":"e_1_3_2_1_8_1","unstructured":"Tabea Bordis. 2025. Scaling Correctness-by-Construction. Ph. D. Dissertation. Karlsruhe Institute of Technology. Karlsruhe. Forthcoming"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-08166-8_5"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2024.3390948"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","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. ACM Magdeburg Germany. 1\u20139. isbn:978-1-4503-7501-6 https:\/\/doi.org\/10.1145\/3377024.3377038 10.1145\/3377024.3377038","DOI":"10.1145\/3377024.3377038"},{"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","DOI":"10.1109\/TR.2015.2452931"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/MITP.2012.39"},{"key":"e_1_3_2_1_15_1","unstructured":"S. Chaki E. Clarke D. Giannakopoulou and C. S. Pasareanu. 2004. Abstraction and Assume-Guarantee Reasoning for Automated Software Verification. https:\/\/ntrs.nasa.gov\/citations\/20050185529"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36577-X_24"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384676"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/DEPCOS-RELCOMEX.2006.13"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_3_2_1_20_1","volume-title":"A discipline of programming. Englewood Cliffs","author":"Dijkstra Edsger Wybe","unstructured":"Edsger Wybe Dijkstra. 1976. A discipline of programming. Englewood Cliffs, N.J. : Prentice-Hall. isbn:978-0-13-215871-8"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/s101070100263"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2577080.2577095"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.23919\/DATE58400.2024.10546852"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2248487.2150982"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","unstructured":"Alcides Fonseca and Guilherme Espada. 2022. Type Systems in Resource-Aware Programming: Opportunities and Challenges. https:\/\/doi.org\/10.48550\/arXiv.2205.15211 10.48550\/arXiv.2205.15211","DOI":"10.48550\/arXiv.2205.15211"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87879-7_8"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2002.1114984"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-8176-4729-2"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-5983-1"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","unstructured":"Juan Pedro Guti\u00e9rrez Hermosillo Muriedas et al. 2023. perun: Benchmarking Energy Consumption of High-Performance Computing Applications. In Euro-Par 2023: Parallel Processing. Springer Nature Switzerland Cham. 17\u201331. isbn:978-3-031-39698-4 https:\/\/doi.org\/10.1007\/978-3-031-39698-4_2 10.1007\/978-3-031-39698-4_2","DOI":"10.1007\/978-3-031-39698-4_2"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2012.6227198"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2013.6606555"},{"key":"e_1_3_2_1_33_1","volume-title":"31st International System Safety Conference. The International System Safety Society Boston, Massachusetts USA, 12\u201316","author":"Hawkins Richard","year":"2013","unstructured":"Richard Hawkins, Ibrahim Habli, and Tim Kelly. 2013. The principles of software safety assurance. In 31st International System Safety Conference. The International System Safety Society Boston, Massachusetts USA, 12\u201316."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48068-4_3"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/QUATIC.2007.8"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.869367"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2597073.2597097"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.748921"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTCSA.2010.42"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","unstructured":"Z. Jelinski and P. Moranda. 1972. Software Reliability Research. In Statistical Computer Performance Evaluation. Academic Press 465\u2013484. isbn:978-0-12-266950-7 https:\/\/doi.org\/10.1016\/B978-0-12-266950-7.50028-1 10.1016\/B978-0-12-266950-7.50028-1","DOI":"10.1016\/B978-0-12-266950-7.50028-1"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/GREENS.2012.6224256"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.future.2018.02.044"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-12466-7_6"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1062455.1062482"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314602"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-61362-4_10"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-75387-9_14"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27919-5"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/TR.2004.832819"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1983.235116"},{"key":"e_1_3_2_1_51_1","unstructured":"J. N. Lyness. 1978. Performance profiles and software evaluation. Argonne National Lab. IL (USA). https:\/\/www.osti.gov\/biblio\/6411646"},{"key":"e_1_3_2_1_52_1","volume-title":"Hermenegildo","author":"L\u00f3pez-Garc\u00eda Pedro","year":"2018","unstructured":"Pedro L\u00f3pez-Garc\u00eda, Luthfi Darmawan, Maximiliano Klemen, Umer Liqat, Francisco Bueno, and Manuel V. Hermenegildo. 2018. Interval-based Resource Usage Verification by Translation into Horn Clauses and an Application to Energy Consumption. CoRR, abs\/1803.04451 (2018), arxiv:1803.04451"},{"key":"e_1_3_2_1_53_1","unstructured":"Main Commission Aircraft Accident Investigation Warsaw. 1994. A320-211 Warsaw Accident Report."},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2021.106560"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.23919\/DATE54114.2022.9774534"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/11889229_4"},{"key":"e_1_3_2_1_57_1","unstructured":"Peter David Miller. 2006. Applied Asymptotic Analysis. American Mathematical Soc.. isbn:978-0-8218-4078-8"},{"key":"e_1_3_2_1_58_1","volume-title":"Programming from specifications","author":"Morgan Carroll","unstructured":"Carroll Morgan. 1990. Programming from specifications. Prentice-Hall, Inc., USA. isbn:978-0-13-726225-0"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1109\/MITP.2008.10"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1016\/0164-1212(79)90023-2"},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1201\/9781315217758"},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90029-3"},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.1997.589224"},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.51594\/csitrj.v5i8.1491"},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2021.102609"},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1109\/GREENS.2015.12"},{"key":"e_1_3_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/369275.369291"},{"key":"e_1_3_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISCA45697.2020.00045"},{"key":"e_1_3_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/2422436.2422470"},{"key":"e_1_3_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17108-6_13"},{"key":"e_1_3_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372020.3391565"},{"key":"e_1_3_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-16722-6_2"},{"key":"e_1_3_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-54997-8_25"},{"key":"e_1_3_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-95497-9_4"},{"key":"e_1_3_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25271-6_10"},{"key":"e_1_3_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03418-4_30"},{"key":"e_1_3_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45314-8_23"},{"key":"e_1_3_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45251-6_35"},{"key":"e_1_3_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-61362-4_11"},{"key":"e_1_3_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03418-4_21"},{"key":"e_1_3_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1109\/92.335012"},{"key":"e_1_3_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-46559-3_2"},{"key":"e_1_3_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.suscom.2010.10.002"},{"key":"e_1_3_2_1_84_1","volume-title":"Taxonomies and toolkits of regular language algorithms","author":"Watson Bruce William","unstructured":"Bruce William Watson. 1995. Taxonomies and toolkits of regular language algorithms. Eindhoven University of Technology, Dept. of Mathematics and Computing Science, Eindhoven. isbn:978-90-386-0396-4"},{"key":"e_1_3_2_1_85_1","doi-asserted-by":"publisher","DOI":"10.1002\/(SICI)1096-908X(199705)9:3<127::AID-SMR149>3.0.CO;2-S"},{"key":"e_1_3_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1145\/337292.337436"},{"key":"e_1_3_2_1_87_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03859-9_10"}],"event":{"name":"Onward! '25: 2025 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software","location":"Singapore Singapore","acronym":"Onward! '25","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGAda ACM Special Interest Group on Ada Programming Language"]},"container-title":["Proceedings of the 2025 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3759429.3762623","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T18:38:00Z","timestamp":1760035080000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3759429.3762623"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":87,"alternative-id":["10.1145\/3759429.3762623","10.1145\/3759429"],"URL":"https:\/\/doi.org\/10.1145\/3759429.3762623","relation":{},"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}