{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:01:38Z","timestamp":1762459298763,"version":"3.40.3"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319223599"},{"type":"electronic","value":"9783319223605"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-319-22360-5_5","type":"book-chapter","created":{"date-parts":[[2015,7,27]],"date-time":"2015-07-27T08:24:42Z","timestamp":1437985482000},"page":"49-62","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Deciding Synchronous Kleene Algebra with Derivatives"],"prefix":"10.1007","author":[{"given":"Sabine","family":"Broda","sequence":"first","affiliation":[]},{"given":"S\u00edlvia","family":"Cavadas","sequence":"additional","affiliation":[]},{"given":"Miguel","family":"Ferreira","sequence":"additional","affiliation":[]},{"given":"Nelma","family":"Moreira","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,28]]},"reference":[{"issue":"1\/2","key":"5_CR1","first-page":"7","volume":"15","author":"M Almeida","year":"2010","unstructured":"Almeida, M., Moreira, N., Reis, R.: Testing regular languages equivalence. J. Automata Lang. Comb. 15(1\/2), 7\u201325 (2010)","journal-title":"J. Automata Lang. Comb."},{"key":"5_CR2","unstructured":"Almeida, R.: Decision algorithms for Kleene algebra with tests and Hoare logic. Master\u2019s thesis, Faculdade de Ci\u00eancias da Universidade do Porto, July 2012. http:\/\/www.dcc.fc.up.pt\/~nam\/web\/resources\/docs\/thesisRA.pdf"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Almeida, R., Broda, S., Moreira, N.: Deciding KAT and Hoare logic with derivatives. In: Faella, M., Murano, A. (eds.) 3rd GANDALF. EPTCS, vol. 96, pp. 127\u2013140 (2012)","DOI":"10.4204\/EPTCS.96.10"},{"issue":"2","key":"5_CR4","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/0304-3975(95)00182-4","volume":"155","author":"VM Antimirov","year":"1996","unstructured":"Antimirov, V.M.: Partial derivatives of regular expressions and finite automaton constructions. Theoret. Comput. Sci. 155(2), 291\u2013319 (1996)","journal-title":"Theoret. Comput. Sci."},{"issue":"2","key":"5_CR5","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0167-6423(92)90005-V","volume":"19","author":"G Berry","year":"1992","unstructured":"Berry, G., Gonthier, G.: The Esterel synchronous programming language: design, semantics, implementation. Sci. Comput. Program. 19(2), 87\u2013152 (1992)","journal-title":"Sci. Comput. Program."},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"Bonchi, F., Pous, D.: Checking NFA equivalence with bisimulations up to congruence. In: Giacobazzi, R., Cousot, R. (eds.) POPL 2013, pp. 457\u2013468. ACM (2013)","DOI":"10.1145\/2480359.2429124"},{"issue":"1","key":"5_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-8(1:16)2012","volume":"8","author":"T Braibant","year":"2012","unstructured":"Braibant, T., Pous, D.: Deciding Kleene algebras in Coq. Log. Methods Comput. Sci. 8(1), 1\u201342 (2012)","journal-title":"Log. Methods Comput. Sci."},{"issue":"5","key":"5_CR8","doi-asserted-by":"publisher","first-page":"969","DOI":"10.1142\/S0129054112400400","volume":"23","author":"S Broda","year":"2012","unstructured":"Broda, S., Machiavelo, A., Moreira, N., Reis, R.: On the average size of Glushkov and partial derivative automata. Int. J. Found. Comput. Sci. 23(5), 969\u2013984 (2012)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/978-3-642-40164-0_10","volume-title":"Fundamentals of Computation Theory","author":"S Broda","year":"2013","unstructured":"Broda, S., Machiavelo, A., Moreira, N., Reis, R.: On the average size of Glushkov and equation automata for $${\\sf {KAT}}$$ expressions. In: G\u0105sieniec, L., Wolter, F. (eds.) FCT 2013. LNCS, vol. 8070, pp. 72\u201383. Springer, Heidelberg (2013)"},{"key":"5_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1007\/978-3-319-08019-2_8","volume-title":"Language, Life, Limits","author":"S Broda","year":"2014","unstructured":"Broda, S., Machiavelo, A., Moreira, N., Reis, R.: On the equivalence of automata for $${\\sf {KAT}}$$-expressions. In: Beckmann, A., Csuhaj-Varj\u00fa, E., Meer, K. (eds.) CiE 2014. LNCS, vol. 8493, pp. 73\u201383. Springer, Heidelberg (2014)"},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-319-19225-3_2","volume-title":"Descriptional Complexity of Formal Systems","author":"S Broda","year":"2015","unstructured":"Broda, S., Machiavelo, A., Moreira, N., Reis, R.: Partial derivative automaton for regular expressions with shuffle. In: Shallit, J., Okhotin, A. (eds.) DCFS 2015. LNCS, vol. 9118, pp. 21\u201332. Springer, Heidelberg (2015)"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/978-3-642-25379-9_11","volume-title":"Certified Programs and Proofs","author":"T Coquand","year":"2011","unstructured":"Coquand, T., Siles, V.: A decision procedure for regular expression equivalence in type theory. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 119\u2013134. Springer, Heidelberg (2011)"},{"key":"5_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1070\/RM1961v016n05ABEH004112","volume":"16","author":"VM Glushkov","year":"1961","unstructured":"Glushkov, V.M.: The abstract theory of automata. Russ. Math. Surv. 16, 1\u201353 (1961)","journal-title":"Russ. Math. Surv."},{"key":"5_CR14","unstructured":"Hopcroft, J., Karp, R.M.: A linear algorithm for testing equivalence of finite automata. Technical report TR 71\u2013114, University of California, Berkeley, California (1971)"},{"issue":"3","key":"5_CR15","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1145\/256167.256195","volume":"19","author":"D Kozen","year":"1997","unstructured":"Kozen, D.: Kleene algebra with tests. Trans. Prog. Lang. Syst. 19(3), 427\u2013443 (1997)","journal-title":"Trans. Prog. Lang. Syst."},{"issue":"1","key":"5_CR16","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1145\/343369.343378","volume":"1","author":"D Kozen","year":"2000","unstructured":"Kozen, D.: On Hoare logic and Kleene algebra with tests. ACM Trans. Comput. Log. 1(1), 60\u201376 (2000)","journal-title":"ACM Trans. Comput. Log."},{"key":"5_CR17","first-page":"117","volume":"24","author":"D Kozen","year":"2003","unstructured":"Kozen, D.: Automata on guarded strings and applications. Mat\u00e9matica Contempor\u00e2nea 24, 117\u2013139 (2003)","journal-title":"Mat\u00e9matica Contempor\u00e2nea"},{"key":"5_CR18","unstructured":"Kozen, D.: On the coalgebraic theory of Kleene algebra with tests. Technical report, Cornell University (2008). http:\/\/hdl.handle.net\/1813\/10173"},{"key":"5_CR19","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/s10817-011-9223-4","volume":"49","author":"A Krauss","year":"2011","unstructured":"Krauss, A., Nipkow, T.: Proof pearl: regular expression equivalence and relation algebra. J. Autom. Reasoning 49, 95\u2013109 (2011)","journal-title":"J. Autom. Reasoning"},{"key":"5_CR20","series-title":"PHI Series in computer science","volume-title":"Communication and concurrency","author":"R Milner","year":"1989","unstructured":"Milner, R.: Communication and concurrency. PHI Series in computer science. Prentice Hall, Upper Saddle River (1989)"},{"key":"5_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/978-3-642-33314-9_7","volume-title":"Relational and Algebraic Methods in Computer Science","author":"N Moreira","year":"2012","unstructured":"Moreira, N., Pereira, D., Melo de Sousa, S.: Deciding regular expressions (in-)equivalence in Coq. In: Kahl, W., Griffin, T.G. (eds.) RAMICS 2012. LNCS, vol. 7560, pp. 98\u2013113. Springer, Heidelberg (2012)"},{"key":"5_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"450","DOI":"10.1007\/978-3-319-08970-6_29","volume-title":"Interactive Theorem Proving","author":"T Nipkow","year":"2014","unstructured":"Nipkow, T., Traytel, D.: Unified decision procedures for regular expression equivalence. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 450\u2013466. Springer, Heidelberg (2014). Archive of Formal Proofs 2014"},{"key":"5_CR23","unstructured":"Pereira, D.: Towards certified program logics for the verification of imperative programs. Ph.D. thesis, University of Porto (2013)"},{"key":"5_CR24","doi-asserted-by":"crossref","unstructured":"Pous, D.: Symbolic algorithms for language equivalence and Kleene algebra with tests. In: Rajamani, S.K., Walker, D. (eds.) 42nd POPL 2015, pp. 357\u2013368. ACM (2015)","DOI":"10.1145\/2676726.2677007"},{"issue":"7","key":"5_CR25","doi-asserted-by":"publisher","first-page":"608","DOI":"10.1016\/j.jlap.2010.07.009","volume":"79","author":"C Prisacariu","year":"2010","unstructured":"Prisacariu, C.: Synchronous Kleene algebra. J. Log. Algebr. Program. 79(7), 608\u2013635 (2010)","journal-title":"J. Log. Algebr. Program."},{"key":"5_CR26","unstructured":"Project FAdo: FAdo: tools for formal languages manipulation. http:\/\/fado.dcc.fc.up.pt\/.(Accessed on 01 April 2015)"},{"key":"5_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"480","DOI":"10.1007\/978-3-642-37064-9_42","volume-title":"Language and Automata Theory and Applications","author":"J Rot","year":"2013","unstructured":"Rot, J., Bonsangue, M., Rutten, J.: Coinductive proof techniques for language equivalence. In: Dediu, A.-H., Mart\u00edn-Vide, C., Truthe, B. (eds.) LATA 2013. LNCS, vol. 7810, pp. 480\u2013492. Springer, Heidelberg (2013)"},{"issue":"2","key":"5_CR28","first-page":"367","volume":"22","author":"A Silva","year":"2012","unstructured":"Silva, A.: Position automata for Kleene algebra with tests. Sci. Ann. Comp. Sci. 22(2), 367\u2013394 (2012)","journal-title":"Sci. Ann. Comp. Sci."},{"key":"5_CR29","unstructured":"Synopsys: Esterel studio. http:\/\/www.synopsys.com\/home.aspx"},{"issue":"6","key":"5_CR30","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1145\/363347.363387","volume":"11","author":"K Thompson","year":"1968","unstructured":"Thompson, K.: Regular expression search algorithm. Commun. ACM 11(6), 410\u2013422 (1968)","journal-title":"Commun. ACM"},{"key":"5_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-642-39274-0_3","volume-title":"Implementation and Application of Automata","author":"M Veanes","year":"2013","unstructured":"Veanes, M.: Applications of symbolic finite automata. In: Konstantinidis, S. (ed.) CIAA 2013. LNCS, vol. 7982, pp. 16\u201323. Springer, Heidelberg (2013)"}],"container-title":["Lecture Notes in Computer Science","Implementation and Application of Automata"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-22360-5_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,15]],"date-time":"2023-02-15T13:46:58Z","timestamp":1676468818000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-22360-5_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319223599","9783319223605"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-22360-5_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"28 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}