{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T13:29:33Z","timestamp":1725542973917},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642113185"},{"type":"electronic","value":"9783642113192"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-11319-2_14","type":"book-chapter","created":{"date-parts":[[2010,1,6]],"date-time":"2010-01-06T00:00:05Z","timestamp":1262736005000},"page":"163-179","source":"Crossref","is-referenced-by-count":8,"title":["Invariant and Type Inference for Matrices"],"prefix":"10.1007","author":[{"given":"Thomas A.","family":"Henzinger","sequence":"first","affiliation":[]},{"given":"Thibaud","family":"Hottelier","sequence":"additional","affiliation":[]},{"given":"Laura","family":"Kov\u00e1cs","sequence":"additional","affiliation":[]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"14_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/978-3-540-69738-1_27","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D. Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T., Majumdar, R., Rybalchenko, A.: Invariant Synthesis for Combined Theories. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 346\u2013362. Springer, Heidelberg (2007)"},{"key":"14_CR2","unstructured":"Birkeland, B.: Calculus and Algebra with MathCad 2000. Haeftad. Studentlitteratur (2000)"},{"issue":"3-4","key":"14_CR3","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1016\/j.jsc.2005.09.007","volume":"41","author":"B. Buchberger","year":"2006","unstructured":"Buchberger, B.: An Algorithm for Finding the Basis Elements of the Residue Class Ring of a Zero Dimensional Polynomial Ideal. J. of Symbolic Computation\u00a041(3-4), 475\u2013511 (2006)","journal-title":"J. of Symbolic Computation"},{"key":"14_CR4","doi-asserted-by":"crossref","DOI":"10.1007\/978-0-387-49159-2","volume-title":"An Introduction to Scientific Computing: Twelve Computational Projects Solved with MATLAB","author":"I. Danaila","year":"2007","unstructured":"Danaila, I., Joly, P., Kaber, S.M., Postel, M.: An Introduction to Scientific Computing: Twelve Computational Projects Solved with MATLAB. Springer, Heidelberg (2007)"},{"key":"14_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bjorner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"Denney, E., Fischer, B.: A Generic Annotation Inference Algorithm for the Safety Certification of Automatically Generated Code. In: GPCE, pp. 121\u2013130 (2006)","DOI":"10.1145\/1173706.1173725"},{"issue":"8","key":"14_CR7","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"E.W. Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded Commands, Nondeterminacy and Formal Derivation of Programs. Communications of the ACM\u00a018(8), 453\u2013457 (1975)","journal-title":"Communications of the ACM"},{"key":"14_CR8","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Qadeer, S.: Predicate Abstraction for Software Verification. In: Proc. of POPL, pp. 191\u2013202 (2002)","DOI":"10.1145\/565816.503291"},{"key":"14_CR9","unstructured":"Golub, G.H., van Loan, C.F.: Matrix Computations. Johns Hopkins Univ. Press (1996)"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"Gopan, D., Reps, T.W., Sagiv, M.: A Framework for Numeric Analysis of Array Operations. In: Proc. of POPL, pp. 338\u2013350 (2005)","DOI":"10.1145\/1047659.1040333"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Gulwani, S., McCloskey, B., Tiwari, A.: Lifting Abstract Interpreters to Quantified Logical Domains. In: Proc. of POPL, pp. 235\u2013246 (2008)","DOI":"10.1145\/1328897.1328468"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Halbwachs, N., Peron, M.: Discovering Properties about Arrays in Simple Programs. In: Proc. of PLDI, pp. 339\u2013348 (2008)","DOI":"10.1145\/1379022.1375623"},{"key":"14_CR13","unstructured":"Hicklin, J., Moler, C., Webb, P., Boisvert, R.F., Miller, B., Pozo, R., Remington, K.: JAMA: A Java Matrix Package (2005), http:\/\/math.nist.gov\/javanumerics\/jama\/"},{"key":"14_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-540-73368-3_23","volume-title":"Computer Aided Verification","author":"R. Jhala","year":"2007","unstructured":"Jhala, R., McMillan, K.L.: Array Abstractions from Proofs. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 193\u2013206. Springer, Heidelberg (2007)"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"Korovin, K.: iProver - An Instantiation-based Theorem Prover for First-order Logic. In: Proc. of IJCAR, pp. 292\u2013298 (2009)","DOI":"10.1007\/978-3-540-71070-7_24"},{"key":"14_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-540-74915-8_19","volume-title":"Computer Science Logic","author":"K. Korovin","year":"2007","unstructured":"Korovin, K., Voronkov, A.: Integrating Linear Arithmetic into Superposition Calculus. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol.\u00a04646, pp. 223\u2013237. Springer, Heidelberg (2007)"},{"key":"14_CR17","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/978-3-540-71070-7_22","volume-title":"Automated Reasoning","author":"L. Kovacs","year":"2008","unstructured":"Kovacs, L.: Aligator: A Mathematica Package for Invariant Generation. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 275\u2013282. Springer, Heidelberg (2008)"},{"key":"14_CR18","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. Kovacs","year":"2008","unstructured":"Kovacs, L.: Reasoning Algebraically About P-Solvable Loops. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 249\u2013264. Springer, Heidelberg (2008)"},{"key":"14_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"470","DOI":"10.1007\/978-3-642-00593-0_33","volume-title":"FASE 2009","author":"L. Kovacs","year":"2009","unstructured":"Kovacs, L., Voronkov, A.: Finding Loop Invariants for Programs over Arrays Using a Theorem Prover. In: Chechik, M., Wirsing, M. (eds.) FASE 2009. LNCS, vol.\u00a05503, pp. 470\u2013485. Springer, Heidelberg (2009)"},{"key":"14_CR20","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Rinard, M.: An overview of the Jahob analysis system: Project goals and current status. In: NSF Next Generation Software Workshop (2006)","DOI":"10.1109\/IPDPS.2006.1639580"},{"key":"14_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/978-3-540-78800-3_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K.L. McMillan","year":"2008","unstructured":"McMillan, K.L.: Quantified Invariant Generation Using an Interpolating Saturation Prover. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 413\u2013427. Springer, Heidelberg (2008)"},{"issue":"5","key":"14_CR22","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1016\/j.ipl.2004.05.004","volume":"91","author":"M. M\u00fcller-Olm","year":"2004","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Computing Polynomial Program Invariants. Indormation Processing Letters\u00a091(5), 233\u2013244 (2004)","journal-title":"Indormation Processing Letters"},{"issue":"2-3","key":"14_CR23","first-page":"91","volume":"15","author":"A. Riazanov","year":"2002","unstructured":"Riazanov, A., Voronkov, A.: The Design and Implementation of Vampire. AI Communications\u00a015(2-3), 91\u2013110 (2002)","journal-title":"AI Communications"},{"issue":"4","key":"14_CR24","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1016\/j.jsc.2007.01.002","volume":"42","author":"E. Rodriguez-Carbonell","year":"2007","unstructured":"Rodriguez-Carbonell, E., Kapur, D.: Generating All Polynomial Invariants in Simple Loops. J. of Symbolic Computation\u00a042(4), 443\u2013476 (2007)","journal-title":"J. of Symbolic Computation"},{"key":"14_CR25","doi-asserted-by":"crossref","unstructured":"Sankaranaryanan, S., Sipma, H.B., Manna, Z.: Non-Linear Loop Invariant Generation using Gr\u00f6bner Bases. In: Proc. of POPL, pp. 318\u2013329 (2004)","DOI":"10.1145\/982962.964028"},{"issue":"2-3","key":"14_CR26","first-page":"111","volume":"15","author":"S. Schulz","year":"2002","unstructured":"Schulz, S.: E \u2014 a brainiac theorem prover. AI Communications\u00a015(2-3), 111\u2013126 (2002)","journal-title":"AI Communications"},{"key":"14_CR27","doi-asserted-by":"crossref","unstructured":"Srivastava, S., Gulwani, S.: Program Verification using Templates over Predicate Abstraction. In: Proc. of PLDI, pp. 223\u2013234 (2009)","DOI":"10.1145\/1543135.1542501"},{"key":"14_CR28","unstructured":"Stewart, G.W.: JAMPACK: A Java Package For Matrix Computations, http:\/\/www.mathematik.hu-berlin.de\/~lamour\/software\/JAVA\/Jampack\/"},{"key":"14_CR29","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G.: The TPTP Problem Library and Associated Infrastructure. The FOF and CNF Parts, v3.5.0. J. of Automated Reasoning (to appear, 2009)","DOI":"10.1007\/s10817-009-9143-8"},{"key":"14_CR30","unstructured":"Wolfram, S.: The Mathematica Book. Version 5.0. Wolfram Media (2003)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-11319-2_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,29]],"date-time":"2023-05-29T07:00:51Z","timestamp":1685343651000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-11319-2_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642113185","9783642113192"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-11319-2_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}