{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T04:06:12Z","timestamp":1725768372385},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642540127"},{"type":"electronic","value":"9783642540134"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54013-4_24","type":"book-chapter","created":{"date-parts":[[2014,1,2]],"date-time":"2014-01-02T20:08:09Z","timestamp":1388693289000},"page":"434-452","source":"Crossref","is-referenced-by-count":3,"title":["Synthesis for Polynomial Lasso Programs"],"prefix":"10.1007","author":[{"given":"Jan","family":"Leike","sequence":"first","affiliation":[]},{"given":"Ashish","family":"Tiwari","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Non-linear loop invariant generation using Gr\u00f6bner bases. In: POPL (2004)","key":"24_CR1","DOI":"10.1145\/964001.964028"},{"doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Tancau, L., Bod\u00edk, R., Saraswat, V., Seshia, S.: Combinatorial sketching for finite programs. In: ASPLOS (2006)","key":"24_CR2","DOI":"10.1145\/1168857.1168907"},{"doi-asserted-by":"crossref","unstructured":"Gulwani, S., Jha, S., Tiwari, A., Venkatesan, R.: Synthesis of loop-free programs. In: PLDI (2011)","key":"24_CR3","DOI":"10.1145\/1993498.1993506"},{"key":"24_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/11538363_18","volume-title":"Computer Science Logic","author":"A. Tiwari","year":"2005","unstructured":"Tiwari, A.: An algebraic approach for the unsatisfiability of nonlinear constraints. In: Ong, L. (ed.) CSL 2005. LNCS, vol.\u00a03634, pp. 248\u2013262. Springer, Heidelberg (2005)"},{"key":"24_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/3-540-07407-4_17","volume-title":"Automata Theory and Formal Languages","author":"G.E. Collins","year":"1975","unstructured":"Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol.\u00a033, pp. 134\u2013183. Springer, Heidelberg (1975)"},{"doi-asserted-by":"crossref","unstructured":"Stengle, G.: A Nullstellensatz and a Positivstellensatz in semialgebraic geometry. Math. Ann. 207 (1974)","key":"24_CR6","DOI":"10.1007\/BF01362149"},{"doi-asserted-by":"crossref","unstructured":"Parrilo, P.A.: Semidefinite programming relaxations for semialgebraic problems. Mathematical Programming Ser. B 96(2) (2003)","key":"24_CR7","DOI":"10.1007\/s10107-003-0387-5"},{"doi-asserted-by":"crossref","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Computing polynomial program invariants. Inf. Process. Lett. 91(5) (2004)","key":"24_CR8","DOI":"10.1016\/j.ipl.2004.05.004"},{"key":"24_CR9","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/BF00268497","volume":"6","author":"M. Karr","year":"1976","unstructured":"Karr, M.: Affine relationships among variables of a program. Acta Informatica\u00a06, 133\u2013151 (1976)","journal-title":"Acta Informatica"},{"key":"24_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-540-69166-2_20","volume-title":"Static Analysis","author":"H. Seidl","year":"2008","unstructured":"Seidl, H., Flexeder, A., Petter, M.: Analysing all polynomial equations in \n                  \n                    \n                  \n                  ${\\mathbb Z_{2^w}}$\n                . In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol.\u00a05079, pp. 299\u2013314. Springer, Heidelberg (2008)"},{"doi-asserted-by":"crossref","unstructured":"Rodr\u00edguez-Carbonell, E., Kapur, D.: Automatic generation of polynomial loop invariants: Algebraic foundations. In: ISSAC. ACM (2004)","key":"24_CR11","DOI":"10.1145\/1005285.1005324"},{"key":"24_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/978-3-540-31862-0_24","volume-title":"Theoretical Aspects of Computing - ICTAC 2004","author":"E. Rodr\u00edguez-Carbonell","year":"2005","unstructured":"Rodr\u00edguez-Carbonell, E., Kapur, D.: Program verification using automatic generation of invariants. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol.\u00a03407, pp. 325\u2013340. Springer, Heidelberg (2005)"},{"doi-asserted-by":"crossref","unstructured":"Col\u00f3n, M.A.: Polynomial approximations of the relational semantics of imperative programs. Sci. Comput. Program. 64(1) (2007)","key":"24_CR13","DOI":"10.1016\/j.scico.2006.03.004"},{"key":"24_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-642-33125-1_7","volume-title":"Static Analysis","author":"D. Cachera","year":"2012","unstructured":"Cachera, D., Jensen, T., Jobin, A., Kirchner, F.: Inference of polynomial invariants for imperative programs: A farewell to Gr\u00f6bner bases. In: Min\u00e9, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol.\u00a07460, pp. 58\u201374. Springer, Heidelberg (2012)"},{"unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: Polyranking for polynomial loops (2005)","key":"24_CR15"},{"key":"24_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/11506676_11","volume-title":"Logic Based Program Synthesis and Transformation","author":"M.A. Col\u00f3n","year":"2005","unstructured":"Col\u00f3n, M.A.: Schema-guided synthesis of imperative programs by constraint solving. In: Etalle, S. (ed.) LOPSTR 2004. LNCS, vol.\u00a03573, pp. 166\u2013181. Springer, Heidelberg (2005)"},{"doi-asserted-by":"crossref","unstructured":"Srivastava, S., Gulwani, S., Foster, J.S.: From program verification to program synthesis. In: POPL 2010, pp. 313\u2013326 (2010)","key":"24_CR17","DOI":"10.1145\/1707801.1706337"},{"unstructured":"Cox, D., Little, J., O\u2019Shea, D.: Ideals, Varieties and Algorithms: An Introduction to Computational Algebraic Geometry and Commutative Algebra. Springer (1991)","key":"24_CR18"},{"issue":"1-3","key":"24_CR19","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1016\/S0022-4049(96)00103-X","volume":"124","author":"R. Neuhaus","year":"1998","unstructured":"Neuhaus, R.: Computation of real radicals of polynomial ideals \u2013 ii. Journal of Pure and Applied Algebra\u00a0124(1-3), 261\u2013280 (1998)","journal-title":"Journal of Pure and Applied Algebra"},{"key":"24_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/978-3-642-31365-3_27","volume-title":"Automated Reasoning","author":"D. Jovanovi\u0107","year":"2012","unstructured":"Jovanovi\u0107, D., de Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol.\u00a07364, pp. 339\u2013354. Springer, Heidelberg (2012)"},{"key":"24_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/978-3-540-85762-4_29","volume-title":"Theoretical Aspects of Computing - ICTAC 2008","author":"R. Rebiha","year":"2008","unstructured":"Rebiha, R., Matringe, N., Moura, A.V.: Endomorphisms for non-trivial non-linear loop invariant generation. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds.) ICTAC 2008. LNCS, vol.\u00a05160, pp. 425\u2013439. Springer, Heidelberg (2008)"},{"doi-asserted-by":"crossref","unstructured":"Adams, W.W., Loustaunau, P.: An Introduction to Gr\u00f6bner Bases. American Mathematical Society (1994)","key":"24_CR22","DOI":"10.1090\/gsm\/003"},{"key":"24_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/3-540-62950-5_65","volume-title":"Rewriting Techniques and Applications","author":"L. Bachmair","year":"1997","unstructured":"Bachmair, L., Tiwari, A.: D-bases for polynomial ideals over commutative noetherian rings. In: Comon, H. (ed.) RTA 1997. LNCS, vol.\u00a01232, pp. 113\u2013127. Springer, Heidelberg (1997)"},{"unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall (1976)","key":"24_CR24"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-54013-4_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,25]],"date-time":"2019-05-25T19:48:19Z","timestamp":1558813699000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54013-4_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642540127","9783642540134"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54013-4_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}