{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,18]],"date-time":"2026-01-18T10:00:51Z","timestamp":1768730451859,"version":"3.49.0"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319465197","type":"print"},{"value":"9783319465203","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-46520-3_30","type":"book-chapter","created":{"date-parts":[[2016,9,21]],"date-time":"2016-09-21T06:40:27Z","timestamp":1474440027000},"page":"479-494","source":"Crossref","is-referenced-by-count":28,"title":["Polynomial Invariants by Linear Algebra"],"prefix":"10.1007","author":[{"given":"Steven","family":"de Oliveira","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Saddek","family":"Bensalem","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Virgile","family":"Prevosto","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,9,22]]},"reference":[{"key":"30_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"467","DOI":"10.1007\/978-3-540-24730-2_35","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Alur","year":"2004","unstructured":"Alur, R., Etessami, K., Madhusudan, P.: A temporal logic of nested calls and returns. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 467\u2013481. Springer, Heidelberg (2004)"},{"issue":"1","key":"30_CR2","doi-asserted-by":"crossref","first-page":"76","DOI":"10.1109\/TSE.1975.6312822","volume":"1","author":"SK Basu","year":"1975","unstructured":"Basu, S.K., Misra, J.: Proving loop programs. IEEE Trans. Softw. Eng. 1(1), 76\u201386 (1975)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"30_CR3","doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Path invariants. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 300\u2013309 (2007)","DOI":"10.1145\/1250734.1250769"},{"key":"30_CR4","doi-asserted-by":"crossref","unstructured":"Botella, B., Delahaye, M., Ha, S.H.T., Kosmatov, N., Mouy, P., Roger, M., Williams, N.: Automating structural testing of C programs: experience with PathCrawler. In: 4th International Workshop on Automation of Software Test, AST, pp. 70\u201378 (2009)","DOI":"10.1109\/IWAST.2009.5069043"},{"key":"30_CR5","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1016\/j.scico.2014.02.028","volume":"93","author":"D Cachera","year":"2014","unstructured":"Cachera, D., Jensen, T.P., Jobin, A., Kirchner, F.: Inference of polynomial invariants for imperative programs: a farewell to Gr\u00f6bner bases. Sci. Comput. Program. 93, 89\u2013109 (2014)","journal-title":"Sci. Comput. Program."},{"key":"30_CR6","unstructured":"Carbonell, E.: Polynomial invariant generation. http:\/\/www.cs.upc.edu\/erodri\/webpage\/polynomial_invariants\/list.html"},{"key":"30_CR7","first-page":"154","volume":"2000","author":"EM Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. CAV 2000, 154\u2013169 (2000)","journal-title":"CAV"},{"issue":"5","key":"30_CR8","doi-asserted-by":"crossref","first-page":"603","DOI":"10.1145\/504709.504710","volume":"23","author":"KD Cooper","year":"2001","unstructured":"Cooper, K.D., Simpson, L.T., Vick, C.A.: Operator strength reduction. ACM Trans. Program. Lang. Syst. 23(5), 603\u2013625 (2001)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"30_CR9","unstructured":"de Oliveira, S., Bensalem, S., Prevosto, V.: Polynomial invariants by linear algebra. Technical report 16\u20130065\/SDO, CEA (2016). http:\/\/steven-de-oliveira.perso.sfr.fr\/content\/publis\/pilat_tech_report.pdf"},{"issue":"10","key":"30_CR10","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"issue":"1","key":"30_CR11","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1145\/602382.602403","volume":"50","author":"CAR Hoare","year":"2003","unstructured":"Hoare, C.A.R.: The verifying compiler: a grand challenge for computing research. J. ACM 50(1), 63\u201369 (2003)","journal-title":"J. ACM"},{"key":"30_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1007\/978-3-642-33386-6_16","volume-title":"Automated Technology for Verification and Analysis","author":"H Hojjat","year":"2012","unstructured":"Hojjat, H., Iosif, R., Kone\u010dn\u00fd, F., Kuncak, V., R\u00fcmmer, P.: Accelerating interpolants. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 187\u2013202. Springer, Heidelberg (2012)"},{"issue":"1","key":"30_CR13","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1137\/0204007","volume":"4","author":"DB Johnson","year":"1975","unstructured":"Johnson, D.B.: Finding all the elementary circuits of a directed graph. SIAM J. Comput. 4(1), 77\u201384 (1975)","journal-title":"SIAM J. Comput."},{"issue":"11","key":"30_CR14","doi-asserted-by":"crossref","first-page":"787","DOI":"10.1016\/j.jsc.2008.03.002","volume":"43","author":"M Kauers","year":"2008","unstructured":"Kauers, M., Zimmermann, B.: Computing the algebraic relations of C-finite sequences and multisequences. J. Symb. Comput. 43(11), 787\u2013803 (2008)","journal-title":"J. Symb. Comput."},{"issue":"3","key":"30_CR15","doi-asserted-by":"crossref","first-page":"573","DOI":"10.1007\/s00165-014-0326-7","volume":"27","author":"F Kirchner","year":"2015","unstructured":"Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. Formal Aspects Comput. 27(3), 573\u2013609 (2015)","journal-title":"Formal Aspects Comput."},{"key":"30_CR16","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/978-3-540-71070-7_22","volume-title":"Automated Reasoning","author":"L Kov\u00e1cs","year":"2008","unstructured":"Kov\u00e1cs, L.: Aligator: a mathematica package for invariant generation (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 275\u2013282. Springer, Heidelberg (2008)"},{"key":"30_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"242","DOI":"10.1007\/978-3-642-11486-1_21","volume-title":"Perspectives of Systems Informatics","author":"L Kov\u00e1cs","year":"2010","unstructured":"Kov\u00e1cs, L.: A complete invariant generation approach for P-solvable loops. In: Pnueli, A., Virbitskaite, I., Voronkov, A. (eds.) PSI 2009. LNCS, vol. 5947, pp. 242\u2013256. Springer, Heidelberg (2010)"},{"key":"30_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"400","DOI":"10.1007\/BFb0029002","volume-title":"STACS 1989","author":"E Mayr","year":"1989","unstructured":"Mayr, E.: Membership in polynomial ideals over Q is exponential space complete. In: Monien, B., Cori, R. (eds.) STACS 1989. LNCS, vol. 349, pp. 400\u2013406. Springer, Heidelberg (1989)"},{"key":"30_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"4","DOI":"10.1007\/3-540-45789-5_4","volume-title":"Static Analysis","author":"M M\u00fcller-Olm","year":"2002","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Polynomial constants are decidable. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 4\u201319. Springer, Heidelberg (2002)"},{"key":"30_CR20","doi-asserted-by":"crossref","first-page":"330","DOI":"10.1145\/964001.964029","volume":"2004","author":"M M\u00fcller-Olm","year":"2004","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra. POPL 2004, 330\u2013341 (2004)","journal-title":"POPL"},{"key":"30_CR21","doi-asserted-by":"crossref","unstructured":"Pan, V.Y., Chen, Z.Q.: The complexity of the matrix eigenproblem. In: Proceedings of the Thirty-First Annual ACM Symposium on Theory of Computing, May 1\u20134, Atlanta, Georgia, USA, pp. 507\u2013516 (1999)","DOI":"10.1145\/301250.301389"},{"issue":"4","key":"30_CR22","doi-asserted-by":"crossref","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. Symbolic Comput. 42(4), 443\u2013476 (2007)","journal-title":"J. Symbolic Comput."},{"issue":"2","key":"30_CR23","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"RE Tarjan","year":"1972","unstructured":"Tarjan, R.E.: Depth-first search and linear graph algorithms. SIAM J. Comput. 1(2), 146\u2013160 (1972)","journal-title":"SIAM J. Comput."}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-46520-3_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,8]],"date-time":"2022-07-08T18:40:37Z","timestamp":1657305637000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-46520-3_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319465197","9783319465203"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-46520-3_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}