{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T07:30:56Z","timestamp":1742974256746,"version":"3.40.3"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030638818"},{"type":"electronic","value":"9783030638825"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-63882-5_12","type":"book-chapter","created":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T14:08:03Z","timestamp":1605794883000},"page":"192-209","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Porting the Software Product Line Refinement Theory to the Coq Proof\u00a0Assistant"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3841-0190","authenticated-orcid":false,"given":"Thayonara","family":"Alves","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6154-1666","authenticated-orcid":false,"given":"Leopoldo","family":"Teixeira","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1573-048X","authenticated-orcid":false,"given":"Vander","family":"Alves","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5758-2097","authenticated-orcid":false,"given":"Thiago","family":"Castro","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,11,19]]},"reference":[{"key":"12_CR1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37521-7","volume-title":"Feature-Oriented Software Product Lines","author":"S Apel","year":"2013","unstructured":"Apel, S., Batory, D., K\u00e4stner, C., Saake, G.: Feature-Oriented Software Product Lines. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37521-7"},{"key":"12_CR2","unstructured":"Bodeveix, J.P., Filali, M., Mun\u00f5z, C.: A formalization of the B method in Coq and PVS. In: FM\u201999 - B Users Group Meeting - Applying B in An Industrial Context: Tools, Lessons and Techniques, pp. 32\u201348. Springer, Cham (1999)"},{"key":"12_CR3","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.tcs.2012.01.031","volume":"455","author":"P Borba","year":"2012","unstructured":"Borba, P., Teixeira, L., Gheyi, R.: A theory of software product line refinement. Theoret. Comput. Sci. 455, 2\u201330 (2012)","journal-title":"Theoret. Comput. Sci."},{"issue":"4","key":"12_CR4","doi-asserted-by":"publisher","first-page":"687","DOI":"10.1007\/s10515-015-0185-3","volume":"23","author":"J B\u00fcrdek","year":"2015","unstructured":"B\u00fcrdek, J., Kehrer, T., Lochau, M., Reuling, D., Kelter, U., Sch\u00fcrr, A.: Reasoning about product-line evolution using complex feature model differences. Autom. Softw. Eng. 23(4), 687\u2013733 (2015). https:\/\/doi.org\/10.1007\/s10515-015-0185-3","journal-title":"Autom. Softw. Eng."},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"Gomes, K., Teixeira, L., Alves, T., Ribeiro, M., Gheyi, R.: Characterizing safe and partially safe evolution scenarios in product lines: an empirical study. In: VaMoS. Association for Computing Machinery (2019)","DOI":"10.1145\/3302333.3302346"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Kang, K., Cohen, S., Hess, J., Novak, W., Peterson, S.: Feature-oriented domain analysis (foda) feasibility study. Technical report. CMU\/SEI-90-TR-21, Software Engineering Institute, Carnegie Mellon University, November 1990","DOI":"10.21236\/ADA235785"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Kr\u00f6her, C., Gerling, L., Schmid, K.: Identifying the intensity of variability changes in software product line evolution. In: SPLC, p. 54\u201364. Association for Computing Machinery (2018)","DOI":"10.1145\/3233027.3233032"},{"key":"12_CR8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71437-8","volume-title":"Software Product Lines in Action: the Best Industrial Practice in Product Line Engineering","author":"F Van der Linden","year":"2007","unstructured":"Van der Linden, F., Schmid, K., Rommes, E.: Software Product Lines in Action: the Best Industrial Practice in Product Line Engineering. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71437-8"},{"key":"12_CR9","unstructured":"Miller, S., Greve, D., Wilding, M., Srivas, M.: Formal verification of the Aamp-Fv microcode. Technical report (1999)"},{"issue":"C","key":"12_CR10","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1016\/j.jss.2015.04.024","volume":"106","author":"L Neves","year":"2015","unstructured":"Neves, L., et al.: Safe evolution templates for software product lines. J. Syst. Softw. 106(C), 42\u201358 (2015)","journal-title":"J. Syst. Softw."},{"key":"12_CR11","unstructured":"Owre, S., Shankar, N., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS Language Reference. SRI International (2001). http:\/\/pvs.csl.sri.com\/doc\/pvs-language-reference.pdf, version 2.4"},{"key":"12_CR12","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/j.jss.2019.04.051","volume":"155","author":"G Sampaio","year":"2019","unstructured":"Sampaio, G., Borba, P., Teixeira, L.: Partially safe evolution of software product lines. J. Syst. Softw. 155, 17\u201342 (2019)","journal-title":"J. Syst. Softw."},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"Spadini, D., Aniche, M., Bacchelli, A.: PyDriller: Python framework for mining software repositories. In: ESEC\/FSE, pp. 908\u2013911. Association for Computing Machinery (2018)","DOI":"10.1145\/3236024.3264598"},{"key":"12_CR14","unstructured":"Team, T.C.D.: The COQ proof assistant reference manual. Technical report, INRIA (2020). https:\/\/coq.inria.fr\/distrib\/current\/refman\/"},{"key":"12_CR15","doi-asserted-by":"crossref","unstructured":"Teixeira, L., Alves, V., Borba, P., Gheyi, R.: A product line of theories for reasoning about safe evolution of product lines. In: SPLC, pp. 161\u2013170. Association for Computing Machinery (2015)","DOI":"10.1145\/2791060.2791105"},{"key":"12_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/3-540-36469-2_15","volume-title":"Mathematical Knowledge Management","author":"F Wiedijk","year":"2003","unstructured":"Wiedijk, F.: Comparing mathematical provers. In: Asperti, A., Buchberger, B., Davenport, J.H. (eds.) MKM 2003. LNCS, vol. 2594, pp. 188\u2013202. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-36469-2_15"}],"container-title":["Lecture Notes in Computer Science","Formal Methods: Foundations and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-63882-5_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,24]],"date-time":"2021-04-24T01:23:46Z","timestamp":1619227426000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-63882-5_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030638818","9783030638825"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-63882-5_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"19 November 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SBMF","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Brazilian Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ouro Preto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Brazil","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 November 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 November 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sbmf2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/sbmf2020.ufop.br\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"17","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"59% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"1","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3 invited talks are also included. The symposium was held virtually due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}