{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T17:19:21Z","timestamp":1725988761438},"publisher-location":"Cham","reference-count":15,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030002497"},{"type":"electronic","value":"9783030002503"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-030-00250-3_3","type":"book-chapter","created":{"date-parts":[[2018,8,30]],"date-time":"2018-08-30T02:56:51Z","timestamp":1535597811000},"page":"30-44","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Left-Eigenvectors Are Certificates of the Orbit Problem"],"prefix":"10.1007","author":[{"given":"Steven","family":"de Oliveira","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Virgile","family":"Prevosto","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Habermehl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Saddek","family":"Bensalem","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,8,30]]},"reference":[{"key":"3_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-319-52234-0_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S Blazy","year":"2017","unstructured":"Blazy, S., B\u00fchler, D., Yakobowski, B.: Structuring abstract interpreters through state and value abstractions. In: Bouajjani, A., Monniaux, D. (eds.) VMCAI 2017. LNCS, vol. 10145, pp. 112\u2013130. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-52234-0_7"},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/978-3-642-14295-6_23","volume-title":"Computer Aided Verification","author":"M Bozga","year":"2010","unstructured":"Bozga, M., Iosif, R., Kone\u010dn\u00fd, F.: Fast acceleration of ultimately periodic relations. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 227\u2013242. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_23"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 238\u2013252. ACM (1977)","DOI":"10.1145\/512950.512973"},{"key":"3_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/978-3-319-46520-3_30","volume-title":"Automated Technology for Verification and Analysis","author":"S Oliveira de","year":"2016","unstructured":"de Oliveira, S., Bensalem, S., Prevosto, V.: Polynomial invariants by linear algebra. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 479\u2013494. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_30"},{"key":"3_CR5","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/978-3-319-68167-2_22","volume-title":"ATVA 2017","author":"S Oliveira de","year":"2017","unstructured":"de Oliveira, S., Bensalem, S., Prevosto, V.: Synthesizing invariants by solving solvable loops. In: D\u2019Souza, D., Narayan Kumar, K. (eds.) ATVA 2017. LNCS, vol. 10482, pp. 327\u2013343. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68167-2_22"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"de Oliveira, S., Prevosto, V., Habermehl, P., Bensalem, S.: Left-eigenvectors are certificates of the orbit problem. http:\/\/steven-de-oliveira.fr\/content\/publis\/certificates_2018.pdf","DOI":"10.1007\/978-3-030-00250-3_3"},{"issue":"2","key":"3_CR7","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1109\/32.908957","volume":"27","author":"MD Ernst","year":"2001","unstructured":"Ernst, M.D., Cockrell, J., Griswold, W.G., Notkin, D.: Dynamically discovering likely program invariants to support program evolution. IEEE Trans. Softw. Eng. 27(2), 99\u2013123 (2001)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"3_CR8","unstructured":"Fijalkow, N., Ohlmann, P., Ouaknine, J., Pouly, A., Worrell, J.: Semialgebraic invariant synthesis for the Kannan-Lipton orbit problem. In: STACS 2017. LIPIcs, vol. 66, pp. 29:1\u201329:13. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2017)"},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-642-37036-6_8","volume-title":"Programming Languages and Systems","author":"J-C Filli\u00e2tre","year":"2013","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3\u2014where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125\u2013128. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Kannan, R., Lipton, R.J.: The orbit problem is decidable. In: Proceedings of the Twelfth Annual ACM Symposium on Theory of Computing, pp. 252\u2013261. ACM (1980)","DOI":"10.1145\/800141.804673"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"Kannan, R., Lipton, R.J.: Polynomial-time algorithm for the orbit problem. J. ACM (JACM) 33(4), 808\u2013821 (1986)","DOI":"10.1145\/6490.6496"},{"key":"3_CR12","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":"3_CR13","doi-asserted-by":"crossref","unstructured":"Rocha, H., Ismail, H., Cordeiro, L., Barreto, R.: Model checking embedded C software using k-induction and invariants. In: 2015 Brazilian Symposium on Computing Systems Engineering (SBESC), pp. 90\u201395. IEEE (2015)","DOI":"10.1109\/SBESC.2015.24"},{"issue":"4","key":"3_CR14","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1016\/j.jsc.2007.01.002","volume":"42","author":"E Rodr\u00edguez-Carbonell","year":"2007","unstructured":"Rodr\u00edguez-Carbonell, E., Kapur, D.: Generating all polynomial invariants in simple loops. J. Symb. Comput. 42(4), 443\u2013476 (2007)","journal-title":"J. Symb. Comput."},{"key":"3_CR15","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1307\/mmj\/1028999247","volume":"12","author":"A Schinzel","year":"1965","unstructured":"Schinzel, A., Zassenhaus, H.: A refinement of two theorems of Kronecker. Michigan Math. J 12, 81\u201385 (1965)","journal-title":"Michigan Math. J"}],"container-title":["Lecture Notes in Computer Science","Reachability Problems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-00250-3_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,23]],"date-time":"2019-10-23T05:50:00Z","timestamp":1571809800000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-00250-3_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030002497","9783030002503"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-00250-3_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}