{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:57:01Z","timestamp":1776333421842,"version":"3.51.2"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030255428","type":"print"},{"value":"9783030255435","type":"electronic"}],"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_7","type":"book-chapter","created":{"date-parts":[[2019,7,12]],"date-time":"2019-07-12T08:03:09Z","timestamp":1562918589000},"page":"97-115","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":23,"title":["Loop Summarization with Rational Vector Addition Systems"],"prefix":"10.1007","author":[{"given":"Jake","family":"Silverman","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zachary","family":"Kincaid","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,7,12]]},"reference":[{"key":"7_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"480","DOI":"10.1007\/978-3-662-49674-9_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Blondin","year":"2016","unstructured":"Blondin, M., Finkel, A., Haase, C., Haddad, S.: Approaching the coverability problem continuously. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 480\u2013496. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_28"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Carbonneaux, Q., Hoffmann, J., Shao, Z.: Compositional certified resource bounds. In: PLDI (2015)","DOI":"10.1145\/2737924.2737955"},{"key":"7_CR3","unstructured":"David, R., Alla, H.: Continuous Petri nets. In: Proceedings of 8th European Workshop on Applications and Theory Petri Nets, pp. 275\u2013294 (1987)"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Dillig, I., Dillig, T., Li, B., McMillan, K.: Inductive invariant generation via abductive inference. In: OOPSLA (2013)","DOI":"10.1145\/2509136.2509511"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Farzan, A., Kincaid, Z.: Compositional recurrence analysis. In: FMCAD (2015)","DOI":"10.1109\/FMCAD.2015.7542253"},{"issue":"1","key":"7_CR6","doi-asserted-by":"crossref","first-page":"1","DOI":"10.3233\/FI-2015-1168","volume":"137","author":"E Fraca","year":"2015","unstructured":"Fraca, E., Haddad, S.: Complexity analysis of continuous Petri nets. Fundam. Inf. 137(1), 1\u201328 (2015)","journal-title":"Fundam. Inf."},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-319-21690-4_20","volume-title":"Computer Aided Verification","author":"A Gurfinkel","year":"2015","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 343\u2013361. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_20"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-319-11439-2_9","volume-title":"Reachability Problems","author":"C Haase","year":"2014","unstructured":"Haase, C., Halfon, S.: Integer vector addition systems with states. In: Ouaknine, J., Potapov, I., Worrell, J. (eds.) RP 2014. LNCS, vol. 8762, pp. 112\u2013124. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11439-2_9"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/978-3-319-89963-3_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Heizmann","year":"2018","unstructured":"Heizmann, M., et al.: Ultimate automizer and the search for perfect interpolants. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 447\u2013451. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_30"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"Hrushovski, E., Ouaknine, J., Pouly, A., Worrell, J.: Polynomial invariants for affine programs. In: Logic in Computer Science, pp. 530\u2013539 (2018)","DOI":"10.1145\/3209108.3209142"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/978-3-319-73721-8_11","volume-title":"In: Verification, Model Checking, and Abstract Interpretation","author":"A Humenberger","year":"2018","unstructured":"Humenberger, A., Jaroschek, M., Kov\u00e1cs, L.: Invariant Generation for Multi-Path Loops with Polynomial Assignments. In: Verification, Model Checking, and Abstract Interpretation. LNCS, vol. 10747, pp. 226\u2013246. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-73721-8_11"},{"issue":"2","key":"7_CR12","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1016\/S0022-0000(69)80011-5","volume":"3","author":"RM Karp","year":"1969","unstructured":"Karp, R.M., Miller, R.E.: Parallel program schemata. J. Comput. Syst. Sci. 3(2), 147\u2013195 (1969)","journal-title":"J. Comput. Syst. Sci."},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Kincaid, Z., Breck, J., Forouhi Boroujeni, A., Reps, T.: Compositional recurrence analysis revisited. In: PLDI (2017)","DOI":"10.1145\/3062341.3062373"},{"issue":"POPL","key":"7_CR14","first-page":"1","volume":"2","author":"Z Kincaid","year":"2018","unstructured":"Kincaid, Z., Cyphert, J., Breck, J., Reps, T.: Non-linear reasoning for invariant synthesis. PACMPL 2(POPL), 1\u201333 (2018)","journal-title":"PACMPL"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-540-78800-3_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Kov\u00e1cs","year":"2008","unstructured":"Kov\u00e1cs, L.: Reasoning algebraically about P-solvable loops. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 249\u2013264. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_18"},{"key":"7_CR16","doi-asserted-by":"crossref","unstructured":"Li, Y., Albarghouthi, A., Kincaid, Z., Gurfinkel, A., Chechik, M.: Symbolic optimization with SMT solvers. In: POPL, pp. 607\u2013618 (2014)","DOI":"10.1145\/2535838.2535857"},{"key":"7_CR17","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-540-89439-1_18","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"D Monniaux","year":"2008","unstructured":"Monniaux, D.: A quantifier elimination algorithm for linear real arithmetic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 243\u2013257. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-89439-1_18"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/978-3-540-24622-0_21","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T Reps","year":"2004","unstructured":"Reps, T., Sagiv, M., Yorsh, G.: Symbolic implementation of the best transformer. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 252\u2013266. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24622-0_21"},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"Rodr\u00edguez-Carbonell, E., Kapur, D.: Automatic generation of polynomial loop invariants: algebraic foundations. In: ISSAC, pp. 266\u2013273 (2004)","DOI":"10.1145\/1005285.1005324"},{"key":"7_CR20","doi-asserted-by":"crossref","unstructured":"Silverman, J., Kincaid, Z.: Loop summarization with rational vector addition systems (extended version). arXiv e-prints. arXiv:1905.06495 , May 2019","DOI":"10.1007\/978-3-030-25543-5_7"},{"key":"7_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"745","DOI":"10.1007\/978-3-319-08867-9_50","volume-title":"Computer Aided Verification","author":"M Sinn","year":"2014","unstructured":"Sinn, M., Zuleger, F., Veith, H.: A simple and scalable static analysis for bound analysis and amortized complexity analysis. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 745\u2013761. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_50"},{"key":"7_CR22","unstructured":"8th International Competition on Software Verification (SV-COMP 2019) (2019). https:\/\/sv-comp.sosy-lab.org\/2019\/"},{"issue":"3","key":"7_CR23","doi-asserted-by":"publisher","first-page":"577","DOI":"10.1145\/322261.322272","volume":"28","author":"RE Tarjan","year":"1981","unstructured":"Tarjan, R.E.: A unified approach to path problems. J. ACM 28(3), 577\u2013593 (1981)","journal-title":"J. ACM"},{"key":"7_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-642-31424-7_17","volume-title":"Computer Aided Verification","author":"A Thakur","year":"2012","unstructured":"Thakur, A., Reps, T.: A method for symbolic computation of abstract operations. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 174\u2013192. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_17"}],"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_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,12,3]],"date-time":"2019-12-03T17:15:56Z","timestamp":1575393356000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-25543-5_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030255428","9783030255435"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-25543-5_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"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)"}}]}}