{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T17:09:44Z","timestamp":1742404184869},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030255428"},{"type":"electronic","value":"9783030255435"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-25543-5_3","type":"book-chapter","created":{"date-parts":[[2019,7,12]],"date-time":"2019-07-12T12:03:09Z","timestamp":1562932989000},"page":"43-63","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Alternating Automata Modulo First Order Theories"],"prefix":"10.1007","author":[{"given":"Radu","family":"Iosif","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiao","family":"Xu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,7,12]]},"reference":[{"issue":"2","key":"3_CR1","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-540-77395-5_10","volume-title":"Runtime Verification","author":"H Barringer","year":"2007","unstructured":"Barringer, H., Rydeheard, D., Havelund, K.: Rule systems for run-time monitoring: from Eagle to RuleR. In: Sokolsky, O., Ta\u015f\u0131ran, S. (eds.) RV 2007. LNCS, vol. 4839, pp. 111\u2013125. Springer, Heidelberg (2007). \n                      https:\/\/doi.org\/10.1007\/978-3-540-77395-5_10"},{"key":"3_CR3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-59207-2","volume-title":"The Classical Decision Problem: Perspectives in Mathematical Logic","author":"E B\u00f6rger","year":"1997","unstructured":"B\u00f6rger, E., Gr\u00e4del, E., Gurevich, Y.: The Classical Decision Problem: Perspectives in Mathematical Logic. Springer, Heidelberg (1997)"},{"issue":"1","key":"3_CR4","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1145\/322234.322243","volume":"28","author":"AK Chandra","year":"1981","unstructured":"Chandra, A.K., Kozen, D.C., Stockmeyer, L.J.: Alternation. J. ACM 28(1), 114\u2013133 (1981)","journal-title":"J. ACM"},{"key":"3_CR5","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/j.entcs.2018.03.017","volume":"336","author":"L D\u2019Antoni","year":"2018","unstructured":"D\u2019Antoni, L., Kincaid, Z., Wang, F.: A symbolic decision procedure for symbolic alternating finite automata. Electron. Notes Theor. Comput. Sci. 336, 79\u201399 (2018). The Thirty-third Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXIII)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"1","key":"3_CR6","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1145\/2775051.2677012","volume":"50","author":"A Farzan","year":"2015","unstructured":"Farzan, A., Kincaid, Z., Podelski, A.: Proof spaces for unbounded parallelism. SIGPLAN Not. 50(1), 407\u2013420 (2015)","journal-title":"SIGPLAN Not."},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Farzan, A., Kincaid, Z., Podelski, A.: Proving liveness of parameterized programs. In: Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2016, pp. 185\u2013196. ACM (2016)","DOI":"10.1145\/2933575.2935310"},{"key":"3_CR8","unstructured":"First Order Alternating Data Automata (FOADA). \n                      https:\/\/github.com\/cathiec\/FOADA"},{"issue":"6","key":"3_CR9","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1145\/2345156.2254112","volume":"47","author":"S Grebenshchikov","year":"2012","unstructured":"Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. SIGPLAN Not. 47(6), 405\u2013416 (2012)","journal-title":"SIGPLAN Not."},{"issue":"2","key":"3_CR10","doi-asserted-by":"publisher","first-page":"637","DOI":"10.2307\/2274706","volume":"56","author":"JY Halpern","year":"1991","unstructured":"Halpern, J.Y.: Presburger arithmetic with unary predicates is \n                      \n                        \n                      \n                      $$\\pi ^1_1$$\n                     complete. J. Symb. Log. 56(2), 637\u2013642 (1991)","journal-title":"J. Symb. Log."},{"key":"3_CR11","unstructured":"Hojjat, H., R\u00fcmmer, P.: Deciding and interpolating algebraic data types by reduction. Technical report. CoRR abs\/1801.02367 (2018). \n                      http:\/\/arxiv.org\/abs\/1801.02367"},{"key":"3_CR12","unstructured":"Includer. \n                      http:\/\/www.fit.vutbr.cz\/research\/groups\/verifit\/tools\/includer\/"},{"key":"3_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-662-49674-9_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Iosif","year":"2016","unstructured":"Iosif, R., Rogalewicz, A., Vojnar, T.: Abstraction refinement and antichains for trace inclusion of infinite state systems. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 71\u201389. Springer, Heidelberg (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-662-49674-9_5"},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-319-89963-3_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Iosif","year":"2018","unstructured":"Iosif, R., Xu, X.: Abstraction refinement for emptiness checking of alternating data automata. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 93\u2013111. Springer, Cham (2018). \n                      https:\/\/doi.org\/10.1007\/978-3-319-89963-3_6"},{"key":"3_CR15","unstructured":"JavaSMT. \n                      https:\/\/github.com\/sosy-lab\/java-smt"},{"issue":"2","key":"3_CR16","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1016\/0304-3975(94)90242-9","volume":"134","author":"M Kaminski","year":"1994","unstructured":"Kaminski, M., Francez, N.: Finite-memory automata. Theor. Comput. Sci. 134(2), 329\u2013363 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"3_CR17","unstructured":"Kincaid, Z.: Parallel proofs for parallel programs. Ph.D. thesis, University of Toronto (2016)"},{"issue":"2","key":"3_CR18","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1145\/2076450.2076472","volume":"55","author":"V Kuncak","year":"2012","unstructured":"Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Software synthesis procedures. Commun. ACM 55(2), 103\u2013111 (2012)","journal-title":"Commun. ACM"},{"issue":"1","key":"3_CR19","doi-asserted-by":"publisher","first-page":"129","DOI":"10.2140\/pjm.1959.9.129","volume":"9","author":"RC Lyndon","year":"1959","unstructured":"Lyndon, R.C.: An interpolation theorem in the predicate calculus. Pacific J. Math. 9(1), 129\u2013142 (1959)","journal-title":"Pacific J. Math."},{"key":"3_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/11817963_14","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2006","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123\u2013136. Springer, Heidelberg (2006). \n                      https:\/\/doi.org\/10.1007\/11817963_14"},{"key":"3_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-319-08867-9_16","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2014","unstructured":"McMillan, K.L.: Lazy annotation revisited. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 243\u2013259. Springer, Cham (2014). \n                      https:\/\/doi.org\/10.1007\/978-3-319-08867-9_16"},{"issue":"2","key":"3_CR22","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G Nelson","year":"1980","unstructured":"Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM 27(2), 356\u2013364 (1980)","journal-title":"J. ACM"},{"key":"3_CR23","unstructured":"Predicate Automata. \n                      https:\/\/github.com\/zkincaid\/duet\/tree\/ark2\/regression\/predicateAutomata"},{"key":"3_CR24","unstructured":"Presburger, M.: \u00dcber die Vollstandigkeit eines gewissen Systems der Arithmetik. Comptes rendus du I Congr\u00e9s des Pays Slaves, Warsaw (1929)"},{"issue":"3","key":"3_CR25","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/s10703-017-0290-y","volume":"51","author":"A Reynolds","year":"2017","unstructured":"Reynolds, A., King, T., Kuncak, V.: Solving quantified linear arithmetic by counterexample-guided instantiation. Form. Methods Syst. Des. 51(3), 500\u2013532 (2017)","journal-title":"Form. Methods Syst. Des."},{"issue":"11","key":"3_CR26","doi-asserted-by":"publisher","first-page":"1212","DOI":"10.1016\/j.jsc.2010.06.005","volume":"45","author":"A Rybalchenko","year":"2010","unstructured":"Rybalchenko, A., Sofronie-Stokkermans, V.: Constraint solving for interpolation. J. Symb. Comput. 45(11), 1212\u20131233 (2010)","journal-title":"J. Symb. Comput."},{"key":"3_CR27","unstructured":"Z3 SMT Solver. \n                      https:\/\/rise4fun.com\/z3"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-25543-5_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,12]],"date-time":"2019-07-12T12:03:52Z","timestamp":1562933032000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-25543-5_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030255428","9783030255435"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-25543-5_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"12 July 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"New York City, NY","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 July 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 July 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav0","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2019\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-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":"258","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":"67","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":"26% - 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":"9","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":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}