{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T15:40:17Z","timestamp":1772206817063,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":33,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,1,11]],"date-time":"2022-01-11T00:00:00Z","timestamp":1641859200000},"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":[[2022,1,17]]},"DOI":"10.1145\/3497775.3503685","type":"proceedings-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T05:20:48Z","timestamp":1641964848000},"page":"68-81","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":19,"title":["A compositional proof framework for FRETish requirements"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0327-9233","authenticated-orcid":false,"given":"Esther","family":"Conrad","sequence":"first","affiliation":[{"name":"NASA Langley Research Center, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7820-7640","authenticated-orcid":false,"given":"Laura","family":"Titolo","sequence":"additional","affiliation":[{"name":"National Institute of Aerospace, USA"}]},{"given":"Dimitra","family":"Giannakopoulou","sequence":"additional","affiliation":[{"name":"NASA Ames Research Center, USA"}]},{"given":"Thomas","family":"Pressburger","sequence":"additional","affiliation":[{"name":"NASA Ames Research Center, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8503-5514","authenticated-orcid":false,"given":"Aaron","family":"Dutle","sequence":"additional","affiliation":[{"name":"NASA Langley Research Center, USA"}]}],"member":"320","published-online":{"date-parts":[[2022,1,11]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/RE.2014.6912279"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_3"},{"key":"e_1_3_2_1_3_1","volume-title":"An Overview of SAL. In 5th NASA Langley Formal Methods Workshop (LFM","author":"Bensalem S.","year":"2000","unstructured":"S. Bensalem , V. Ganesh , Y. Lakhnech , C. Mu\u00f1oz , S. Owre , H. Rue\u00df , J. Rushby , V. Rusu , H. Sa\u00efdi , N. Shankar , E. Singerman , and A. Tiwari . 2000 . An Overview of SAL. In 5th NASA Langley Formal Methods Workshop (LFM 2000 ). 187\u2013196. S. Bensalem, V. Ganesh, Y. Lakhnech, C. Mu\u00f1oz, S. Owre, H. Rue\u00df, J. Rushby, V. Rusu, H. Sa\u00efdi, N. Shankar, E. Singerman, and A. Tiwari. 2000. An Overview of SAL. In 5th NASA Langley Formal Methods Workshop (LFM 2000). 187\u2013196."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/SYSCON.2018.8369502"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41591-8_24"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050046"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1181775.1181801"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/RE.2017.54"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.329.3"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/302405.302672"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-57288-8_30"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40648-0_4"},{"key":"e_1_3_2_1_13_1","volume-title":"Requirements Engineering: Foundation for Software Quality (REFSQ","author":"Giannakopoulou D.","year":"2020","unstructured":"D. Giannakopoulou , T. Pressburger , A. Mavridou , J. Rhein , J. Schumann , and N. Shi . 2020 . Formal Requirements Elicitation with FRET. In Joint Proceedings of REFSQ-2020 Workshops, Doctoral Symposium, Live Studies Track, and Poster Track co-located with the 26th International Conference on Requirements Engineering: Foundation for Software Quality (REFSQ 2020). D. Giannakopoulou, T. Pressburger, A. Mavridou, J. Rhein, J. Schumann, and N. Shi. 2020. Formal Requirements Elicitation with FRET. In Joint Proceedings of REFSQ-2020 Workshops, Doctoral Symposium, Live Studies Track, and Poster Track co-located with the 26th International Conference on Requirements Engineering: Foundation for Software Quality (REFSQ 2020)."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44429-7_2"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2021.106590"},{"key":"e_1_3_2_1_16_1","unstructured":"E. Jahier P. Raymond and N. Hawlbwachs. 2020. The Lustre V6 Reference Manual.  E. Jahier P. Raymond and N. Hawlbwachs. 2020. The Lustre V6 Reference Manual."},{"key":"e_1_3_2_1_17_1","volume-title":"8th European Congress on Embedded Real Time Software and Systems (ERTS","author":"Jeannet B.","year":"2016","unstructured":"B. Jeannet and F. Gaucher . 2016. Debugging Embedded Systems Requirements with STIMULUS: an Automotive Case-Study . In 8th European Congress on Embedded Real Time Software and Systems (ERTS 2016 ). https:\/\/hal.archives-ouvertes.fr\/hal-01292286 B. Jeannet and F. Gaucher. 2016. Debugging Embedded Systems Requirements with STIMULUS: an Automotive Case-Study. In 8th European Congress on Embedded Real Time Software and Systems (ERTS 2016). https:\/\/hal.archives-ouvertes.fr\/hal-01292286"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1062455.1062526"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01995674"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/RE.2019.00033"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-57288-8_31"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/RE.2009.9"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0218194004001567"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61474-5_99"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/REW.2019.00027"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55602-8_217"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27705-4_18"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2012.02.041"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1155\/2011\/869182"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/DASC.2017.8102059"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2002.1007952"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.6094\/UNIFR\/10633"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/RE.2017.38"}],"event":{"name":"CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs","location":"Philadelphia PA USA","acronym":"CPP '22","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3497775.3503685","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3497775.3503685","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:49:25Z","timestamp":1750193365000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3497775.3503685"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,11]]},"references-count":33,"alternative-id":["10.1145\/3497775.3503685","10.1145\/3497775"],"URL":"https:\/\/doi.org\/10.1145\/3497775.3503685","relation":{},"subject":[],"published":{"date-parts":[[2022,1,11]]},"assertion":[{"value":"2022-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}