{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:48:05Z","timestamp":1772164085510,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":44,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017,1]]},"DOI":"10.1145\/3009837.3009844","type":"proceedings-article","created":{"date-parts":[[2016,12,22]],"date-time":"2016-12-22T16:20:29Z","timestamp":1482423629000},"page":"232-245","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Monadic second-order logic on finite sequences"],"prefix":"10.1145","author":[{"given":"Loris","family":"D'Antoni","sequence":"first","affiliation":[{"name":"University of Wisconsin-Madison, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Margus","family":"Veanes","sequence":"additional","affiliation":[{"name":"Microsoft Research, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,1]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/11605157_3"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1137\/0107041"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1978.1675141"},{"key":"e_1_3_2_1_4_1","first-page":"1982","volume-title":"Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence, IJCAI \u201913","author":"Alur R.","unstructured":"R. Alur , L. D\u2019Antoni , S. Gulwani , D. Kini , and M. Viswanathan . Automated grading of DFA constructions . In Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence, IJCAI \u201913 , pages 1976\u2013 1982 . AAAI Press, 2013. R. Alur, L. D\u2019Antoni, S. Gulwani, D. Kini, and M. Viswanathan. Automated grading of DFA constructions. In Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence, IJCAI \u201913, pages 1976\u20131982. AAAI Press, 2013."},{"key":"e_1_3_2_1_5_1","volume-title":"https:\/\/github.com\/AutomataDotNet\/Automata","year":"2015","unstructured":"Automata. https:\/\/github.com\/AutomataDotNet\/Automata , 2015 . Automata. https:\/\/github.com\/AutomataDotNet\/Automata, 2015."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008699807402"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008644009416"},{"key":"e_1_3_2_1_8_1","unstructured":"Extended version of: \u201cHardware verification using monadic second-order logic \u201d CAV \u201995 LNCS 939.  Extended version of: \u201cHardware verification using monadic second-order logic \u201d CAV \u201995 LNCS 939."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19600060105"},{"key":"e_1_3_2_1_11_1","series-title":"Studies in Logic and the Foundation of Mathematics","volume-title":"Model Theory","author":"Chang C. C.","year":"1990","unstructured":"C. C. Chang and H. J. Keisler . Model Theory , volume 73 of Studies in Logic and the Foundation of Mathematics . North Holland , third edition, 1990 . C. C. Chang and H. J. Keisler. Model Theory, volume 73 of Studies in Logic and the Foundation of Mathematics. North Holland, third edition, 1990."},{"key":"e_1_3_2_1_12_1","first-page":"15","volume-title":"IWLS93: International Workshop on Logic Synthesis","author":"Clarke E.","year":"1993","unstructured":"E. Clarke , M. Fujita , P. McGeer , K. McMillan , and J. Yang . Multiterminal binary decision diagrams: An efficient data structure for matrix representation . In IWLS93: International Workshop on Logic Synthesis , pages 6a:1\u2013 15 , Lake Tahoe, CA , May 1993 . E. Clarke, M. Fujita, P. McGeer, K. McMillan, and J. Yang. Multiterminal binary decision diagrams: An efficient data structure for matrix representation. In IWLS93: International Workshop on Logic Synthesis, pages 6a:1\u201315, Lake Tahoe, CA, May 1993."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/157485.164569"},{"key":"e_1_3_2_1_14_1","volume-title":"Model Checking","author":"Clarke E. M.","year":"1999","unstructured":"E. M. Clarke , O. Grumberg , and D. A. Peled . Model Checking . MIT Press , 1999 . E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 1999."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90268-2"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/647768.733938"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535849"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2791292"},{"key":"e_1_3_2_1_19_1","first-page":"860","volume-title":"Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence, IJCAI \u201913","author":"De Giacomo G.","unstructured":"G. De Giacomo and M. Y. Vardi . Linear temporal logic and linear dynamic logic on finite traces . In Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence, IJCAI \u201913 , pages 854\u2013 860 . AAAI Press, 2013. G. De Giacomo and M. Y. Vardi. Linear temporal logic and linear dynamic logic on finite traces. In Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence, IJCAI \u201913, pages 854\u2013860. AAAI Press, 2013."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1995376.1995394"},{"key":"e_1_3_2_1_22_1","volume-title":"TACAS","author":"De Wulf M.","year":"2008","unstructured":"M. De Wulf , L. Doyen , N. Maquet , and J. F. Raskin . TACAS 2008 , chapter Antichains : Alternative Algorithms for LTL Satisfiability and Model-Checking, pages 63\u201377. Springer Berlin Heidelberg, Berlin, Heidelberg, 2008. M. De Wulf, L. Doyen, N. Maquet, and J. F. Raskin. TACAS 2008, chapter Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking, pages 63\u201377. Springer Berlin Heidelberg, Berlin, Heidelberg, 2008."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_59"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008647823331"},{"key":"e_1_3_2_1_25_1","volume-title":"Symbolic strategy synthesis for games with LTL winning conditions. Technical report","author":"Harding A.","year":"2005","unstructured":"A. Harding . Symbolic strategy synthesis for games with LTL winning conditions. Technical report , 2005 . A. Harding. Symbolic strategy synthesis for games with LTL winning conditions. Technical report, 2005."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/646479.693761"},{"key":"e_1_3_2_1_27_1","volume-title":"USENIX Security","author":"Hooimeijer P.","year":"2011","unstructured":"P. Hooimeijer , B. Livshits , D. Molnar , P. Saxena , and M. Veanes . Fast and precise sanitizer analysis with Bek . In USENIX Security , August 2011 . P. Hooimeijer, B. Livshits, D. Molnar, P. Saxena, and M. Veanes. Fast and precise sanitizer analysis with Bek. In USENIX Security, August 2011."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/258915.258936"},{"key":"e_1_3_2_1_29_1","first-page":"117","volume-title":"Proceedings of the Decennial Caltech Conference on VLSI on Advanced Research in VLSI","author":"Karplus K.","unstructured":"K. Karplus . Using if-then-else DAGs for multi-level logic minimization . In Proceedings of the Decennial Caltech Conference on VLSI on Advanced Research in VLSI , pages 101\u2013 117 . MIT Press, 1989. K. Karplus. Using if-then-else DAGs for multi-level logic minimization. In Proceedings of the Decennial Caltech Conference on VLSI on Advanced Research in VLSI, pages 101\u2013117. MIT Press, 1989."},{"key":"e_1_3_2_1_30_1","volume-title":"Department of Computer Science","author":"Klarlund N.","year":"2001","unstructured":"N. Klarlund and A. M\u00f8ller . MONA Version 1.4 User Manual. BRICS , Department of Computer Science , University of Aarhus , January 2001 . N. Klarlund and A. M\u00f8ller. MONA Version 1.4 User Manual. BRICS, Department of Computer Science, University of Aarhus, January 2001."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/647267.760182"},{"key":"e_1_3_2_1_32_1","first-page":"117","article-title":"Automata on guarded strings and applications","volume":"24","author":"Kozen D.","year":"2003","unstructured":"D. Kozen . Automata on guarded strings and applications . Mat\u00e9matica Contempor\u02c6anea , 24 : 117 \u2013 139 , 2003 . D. Kozen. Automata on guarded strings and applications. Mat\u00e9matica Contempor\u02c6anea, 24:117\u2013139, 2003.","journal-title":"Mat\u00e9matica Contempor\u02c6anea"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1002\/j.1538-7305.1959.tb01585.x"},{"key":"e_1_3_2_1_34_1","volume-title":"Springer Berlin Heidelberg","author":"Madhusudan P.","year":"2011","unstructured":"P. Madhusudan and X. Qiu . Efficient Decision Procedures for Heaps Using STRAND, pages 43\u201359 . Springer Berlin Heidelberg , Berlin, Heidelberg , 2011 . P. Madhusudan and X. Qiu. Efficient Decision Procedures for Heaps Using STRAND, pages 43\u201359. Springer Berlin Heidelberg, Berlin, Heidelberg, 2011."},{"key":"e_1_3_2_1_35_1","volume-title":"Kluwer Academic Publishers","author":"McMillan K. L.","year":"1993","unstructured":"K. L. McMillan . Symbolic Model Checking . Kluwer Academic Publishers , 1993 . K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993."},{"key":"e_1_3_2_1_36_1","volume-title":"USA","author":"Meyer A. R.","year":"1973","unstructured":"A. R. Meyer . Weak monadic second order theory of successor is not elementary-recursive. Technical report, Cambridge, MA , USA , 1973 . A. R. Meyer. Weak monadic second order theory of successor is not elementary-recursive. Technical report, Cambridge, MA, USA, 1973."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1013560.1013562"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/765568.765571"},{"key":"e_1_3_2_1_39_1","volume-title":"Springer Berlin Heidelberg","author":"Rozier K. Y.","year":"2007","unstructured":"K. Y. Rozier and M. Y. Vardi . LTL Satisfiability Checking, pages 149\u2013 167 . Springer Berlin Heidelberg , Berlin, Heidelberg , 2007 . K. Y. Rozier and M. Y. Vardi. LTL Satisfiability Checking, pages 149\u2013 167. Springer Berlin Heidelberg, Berlin, Heidelberg, 2007."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-010-0168-4"},{"key":"e_1_3_2_1_41_1","volume-title":"Springer","author":"Thomas W.","year":"1996","unstructured":"W. Thomas . Languages, automata, and logic. In Handbook of Formal Languages, pages 389\u2013455 . Springer , 1996 . W. Thomas. Languages, automata, and logic. In Handbook of Formal Languages, pages 389\u2013455. Springer, 1996."},{"key":"e_1_3_2_1_42_1","volume-title":"24th EACSL Annual Conference on Computer Science Logic, CSL 2015","author":"Traytel D.","year":"2015","unstructured":"D. Traytel . A coalgebraic decision procedure for WS1S . In 24th EACSL Annual Conference on Computer Science Logic, CSL 2015 , September 7-10, 2015 , Berlin, Germany, pages 487\u2013503 , 2015. D. Traytel. A coalgebraic decision procedure for WS1S. In 24th EACSL Annual Conference on Computer Science Logic, CSL 2015, September 7-10, 2015, Berlin, Germany, pages 487\u2013503, 2015."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39274-0_3"},{"key":"e_1_3_2_1_44_1","first-page":"36","volume-title":"Extended finite state models of language","author":"Watson B. W.","year":"1999","unstructured":"B. W. Watson . Implementing and using finite automata toolkits . In Extended finite state models of language , pages 19\u2013 36 , New York, NY , USA, 1999 . Cambridge University Press . B. W. Watson. Implementing and using finite automata toolkits. In Extended finite state models of language, pages 19\u201336, New York, NY, USA, 1999. Cambridge University Press."}],"event":{"name":"POPL '17: The 44th Annual ACM SIGPLAN Symposium on Principles of Programming Languages","location":"Paris France","acronym":"POPL '17","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3009837.3009844","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3009837.3009844","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:36:21Z","timestamp":1750203381000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3009837.3009844"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1]]},"references-count":44,"alternative-id":["10.1145\/3009837.3009844","10.1145\/3009837"],"URL":"https:\/\/doi.org\/10.1145\/3009837.3009844","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3093333.3009844","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2017,1]]},"assertion":[{"value":"2017-01-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}