{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T12:40:58Z","timestamp":1725540058027},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642046384"},{"type":"electronic","value":"9783642046391"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-04639-1_17","type":"book-chapter","created":{"date-parts":[[2009,11,3]],"date-time":"2009-11-03T08:37:25Z","timestamp":1257237445000},"page":"242-259","source":"Crossref","is-referenced-by-count":0,"title":["Relational Methods in the Analysis of While Loops: Observations of Versatility"],"prefix":"10.1007","author":[{"given":"Asma","family":"Louhichi","sequence":"first","affiliation":[]},{"given":"Olfa","family":"Mraihi","sequence":"additional","affiliation":[]},{"given":"Lamia Labed","family":"Jilani","sequence":"additional","affiliation":[]},{"given":"Khaled","family":"Bsaies","sequence":"additional","affiliation":[]},{"given":"Ali","family":"Mili","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"Fu, J., Bastani, F.B., Yen, I.L.: Automated discovery of loop invariants for high assurance programs synthesized using ai planning techniques. In: HASE 2008: 11th High Assurance Systems Engineering Symposium, Nanjing, China, pp. 333\u2013342 (2008)","DOI":"10.1109\/HASE.2008.36"},{"key":"17_CR2","first-page":"125","volume":"80","author":"J. Carette","year":"2007","unstructured":"Carette, J., Janicki, R.: Computing properties of numeric iterative programs by symbolic computation. Fundamentae Informatica\u00a080, 125\u2013146 (2007)","journal-title":"Fundamentae Informatica"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: Proceedings, 19th Annual Symposium on Logic in Computer Science, pp. 132\u2013144 (2004)","DOI":"10.1109\/LICS.2004.1319598"},{"key":"17_CR4","volume-title":"Proceedings of 11th Working Conference on Reverse Engineering","author":"L. Hu","year":"2004","unstructured":"Hu, L., Harman, M., Hierons, R., Binkley, D.: Loop squashing transformations for amorphous slicing. In: Proceedings of 11th Working Conference on Reverse Engineering. IEEE Computer Society, Los Alamitos (2004)"},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C.: The Daikon system for dynamic detection of likely invariants. Science of Computer Programming (2006)","DOI":"10.1016\/j.scico.2007.01.015"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"Denney, E., Fischer, B.: A generic annotation inference algorithm for the safety certification of automatically generated code. In: Proceedings of the Fifth International Conference on Generative programming and Component Engineering, Portland, Oregon (2006)","DOI":"10.1145\/1173706.1173725"},{"key":"17_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1007\/978-3-540-31862-0_24","volume-title":"Theoretical Aspects of Computing - ICTAC 2004","author":"E.R. Carbonnell","year":"2005","unstructured":"Carbonnell, E.R., 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)"},{"key":"17_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"420","DOI":"10.1007\/978-3-540-45069-6_39","volume-title":"Computer Aided Verification","author":"M.A. Colon","year":"2003","unstructured":"Colon, M.A., Sankaranarayana, S., Sipma, H.B.: Linear invariant generation using non linear constraint solving. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 420\u2013432. Springer, Heidelberg (2003)"},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"Sankaranarayana, S., Sipma, H.B., Manna, Z.: Non linear loop invariant generation using groebner bases. In: Proceedings of ACM SIGPLAN Principles of Programming Languages, POPL 2004, pp. 381\u2013329 (2004)","DOI":"10.1145\/982962.964028"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"Kovacs, L., Jebelean, T.: An algorithm for automated generation of invariants for loops with conditionals. In: Petcu, D. (ed.) Proceedings of the Computer-Aided Verification on Information Systems Workshop (CAVIS 2005), 7th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2005), Department of Computer Science, West University of Timisoara, Romania, pp. 16\u201319 (2005)","DOI":"10.1109\/SYNASC.2005.19"},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"Mili, A., Aharon, S., Nadkarni, C., Mraihi, O., Louhichi, A., Jilani, L.L.: Reflexive transitive invariant relations: A basis for computing loop functions. Journal of Symbolic Computation (2009)","DOI":"10.1016\/j.jsc.2008.11.007"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Mili, A., Desharnais, J., Gagne, J.R.: Strongest invariant functions: Their use in the systematic analysis of while statements. Acta Informatica (1985)","DOI":"10.1007\/BF00290145"},{"key":"17_CR13","volume-title":"Structured programming","author":"R. Linger","year":"1979","unstructured":"Linger, R., Mills, H., Witt, B.: Structured programming. Addison-Wesley, Reading (1979)"},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"Mills, H.: The new math of computer programming. Communications of the ACM 18 (1975)","DOI":"10.1145\/360569.360659"},{"key":"17_CR15","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-5983-1","volume-title":"The Science of programming","author":"D. Gries","year":"1981","unstructured":"Gries, D.: The Science of programming. Springer, Heidelberg (1981)"},{"key":"17_CR16","series-title":"International Series in Computer Sciences","volume-title":"Programming from Specifications","author":"C. Morgan","year":"1998","unstructured":"Morgan, C.: Programming from Specifications. International Series in Computer Sciences. Prentice Hall, London (1998)"},{"key":"17_CR17","volume-title":"A Discipline of Programming","author":"E. Dijkstra","year":"1976","unstructured":"Dijkstra, E.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)"},{"key":"17_CR18","volume-title":"A Mathematical Theory of Computation","author":"Z. Manna","year":"1974","unstructured":"Manna, Z.: A Mathematical Theory of Computation. McGraw-Hill, New York (1974)"},{"key":"17_CR19","doi-asserted-by":"publisher","first-page":"544","DOI":"10.1007\/BF01211474","volume":"4","author":"N. Boudriga","year":"1992","unstructured":"Boudriga, N., Elloumi, F., Mili, A.: The lattice of specifications: Applications to a specification methodology. Formal Aspects of Computing\u00a04, 544\u2013571 (1992)","journal-title":"Formal Aspects of Computing"},{"key":"17_CR20","unstructured":"Mili, A., Aharon, S., Nadkarni, C.: Mathematics for reasoning about loop functions. Technical report, New Jersey Institute of Technology (2008), http:\/\/web.njit.edu\/~mili\/scp.pdf"},{"key":"17_CR21","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1016\/j.jlap.2005.04.006","volume":"66","author":"J. Desharnais","year":"2006","unstructured":"Desharnais, J., Mueller, B., Tchier, F.: Kleene under a modal demonic star. Journal of Logic and Algebraic Programming\u00a066, 127\u2013160 (2006)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"17_CR22","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1109\/TSE.1984.5010236","volume":"10","author":"D. Dunlop","year":"1984","unstructured":"Dunlop, D., Basili, V.R.: A heuristic for deriving loop functions. IEEE Transactions on Software Engineering\u00a010, 275\u2013285 (1984)","journal-title":"IEEE Transactions on Software Engineering"}],"container-title":["Lecture Notes in Computer Science","Relations and Kleene Algebra in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-04639-1_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,27]],"date-time":"2023-05-27T07:16:06Z","timestamp":1685171766000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-04639-1_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642046384","9783642046391"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-04639-1_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}