{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T05:58:57Z","timestamp":1743055137334,"version":"3.40.3"},"publisher-location":"Cham","reference-count":11,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031781155"},{"type":"electronic","value":"9783031781162"}],"license":[{"start":{"date-parts":[[2024,11,29]],"date-time":"2024-11-29T00:00:00Z","timestamp":1732838400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,29]],"date-time":"2024-11-29T00:00:00Z","timestamp":1732838400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-78116-2_7","type":"book-chapter","created":{"date-parts":[[2024,11,28]],"date-time":"2024-11-28T07:31:36Z","timestamp":1732779096000},"page":"107-119","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Brzozowski\u2019s Algorithm for Automata Minimization Verified in Coq"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-9972-9742","authenticated-orcid":false,"given":"Filipe","family":"Ramos","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5194-5870","authenticated-orcid":false,"given":"Karina Girardi","family":"Roggia","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0723-231X","authenticated-orcid":false,"given":"Rafael Castro G.","family":"Silva","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,11,29]]},"reference":[{"key":"7_CR1","unstructured":"Athalye, A.: CoqIOA: a Formalization of IO Automata in the Coq Proof Assistant. Ph.D. thesis, Massachusetts Institute of Technology (2017). https:\/\/dspace.mit.edu\/handle\/1721.1\/112831"},{"key":"7_CR2","volume-title":"Interactive Theorem Proving and Program Development: Coq\u2019Art The Calculus of Inductive Constructions","author":"Y Bertot","year":"2010","unstructured":"Bertot, Y., Castran, P.: Interactive Theorem Proving and Program Development: Coq\u2019Art The Calculus of Inductive Constructions, 1st edn. Springer Publishing Company, Incorporated (2010)","edition":"1"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Bonchi, F., Bonsangue, M.M., Rutten, J.J., Silva, A.: Brzozowski\u2019s algorithm (co) algebraically. In: Logic and Program Semantics, pp. 12\u201323. Springer (2012), https:\/\/link.springer.com\/chapter\/10.1007\/978-3-642-29485-3_2","DOI":"10.1007\/978-3-642-29485-3_2"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Braibant, T., Pous, D.: Deciding Kleene algebras in Coq. Logic. Methods Comput. Sci. 8, (2012). https:\/\/lmcs.episciences.org\/1043","DOI":"10.2168\/LMCS-8(1:16)2012"},{"key":"7_CR5","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-68612-7","volume-title":"Introduction to Discrete Event Systems","author":"CG Cassandras","year":"2008","unstructured":"Cassandras, C.G., Lafortune, S.: Introduction to Discrete Event Systems, 2nd edn. Springer Science+Business Media, New York (2008)","edition":"2"},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"Doczkal, C., Kaiser, J.O., Smolka, G.: A constructive theory of regular languages in Coq. In: International Conference on Certified Programs and Proofs. pp. 82\u201397. Springer (2013). https:\/\/link.springer.com\/chapter\/10.1007\/978-3-319-03545-1_6","DOI":"10.1007\/978-3-319-03545-1_6"},{"key":"7_CR7","volume-title":"Introduction to Automata Theory, Languages, and Computation","author":"JE Hopcroft","year":"2006","unstructured":"Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation, 3rd edn. Pearson\/Addison Wesley, Boston (2006)","edition":"3"},{"key":"7_CR8","unstructured":"Jan, H.: Proof of Brzozowski\u2019s Algorithm for DFA Minimization (2019). https:\/\/cs.stackexchange.com\/questions\/105574\/proof-of-brzozowskis-algorithm-for-dfa-minimization"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Paulson, L.C.: A formalisation of finite automata using hereditarily finite sets. In: International Conference on Automated Deduction, pp. 231\u2013245. Springer (2015). https:\/\/link.springer.com\/chapter\/10.1007\/978-3-319-21401-6_15","DOI":"10.1007\/978-3-319-21401-6_15"},{"key":"7_CR10","unstructured":"Pierce, B.C., et al.: Logical Foundations, vol. 1, 6.6 edn. UPenn CIS, Pennsylvania (2024)"},{"key":"7_CR11","unstructured":"Ramos, F.: Prova da minimiza\u00e7\u00e3o de aut\u00f4matos finitos determin\u00edsticos pelo algoritmo de brzozowski assistida por computador (2021). https:\/\/pergamumweb.udesc.br\/acervo\/152736. supervisors: Karina Girardi Roggia, Rafael Castro G. Silva"}],"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-031-78116-2_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,28]],"date-time":"2024-11-28T09:04:44Z","timestamp":1732784684000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-78116-2_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,29]]},"ISBN":["9783031781155","9783031781162"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-78116-2_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,11,29]]},"assertion":[{"value":"29 November 2024","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":"Vit\u00f3ria","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":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 December 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 December 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sbmf2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}