{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,14]],"date-time":"2024-08-14T11:13:55Z","timestamp":1723634035433},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2012,8,14]],"date-time":"2012-08-14T00:00:00Z","timestamp":1344902400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2012,9]]},"DOI":"10.1007\/s11334-012-0189-0","type":"journal-article","created":{"date-parts":[[2012,8,13]],"date-time":"2012-08-13T14:31:19Z","timestamp":1344868279000},"page":"195-212","source":"Crossref","is-referenced-by-count":3,"title":["Invariant relations, invariant functions, and loop functions"],"prefix":"10.1007","volume":"8","author":[{"given":"Lamia","family":"Labed Jilani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Asma","family":"Louhichi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Olfa","family":"Mraihi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ali","family":"Mili","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,8,14]]},"reference":[{"key":"189_CR1","doi-asserted-by":"crossref","DOI":"10.1007\/b102311","volume-title":"Loop transformations for restructuring compilers","author":"U Banerjee","year":"1993","unstructured":"Banerjee U (1993) Loop transformations for restructuring compilers. Kluwer Academic Publishers, Boston, MA"},{"issue":"1","key":"189_CR2","doi-asserted-by":"crossref","first-page":"76","DOI":"10.1109\/TSE.1975.6312822","volume":"1","author":"SK Basu","year":"1975","unstructured":"Basu SK, Misra JD (1975) Proving loop programs. IEEE Trans Softw Eng 1(1): 76\u201386","journal-title":"IEEE Trans Softw Eng"},{"key":"189_CR3","doi-asserted-by":"crossref","first-page":"544","DOI":"10.1007\/BF01211474","volume":"4","author":"N Boudriga","year":"1992","unstructured":"Boudriga N, Elloumi F, Mili A (1992) The lattice of specifications: applications to a specification methodology. Form Asp Comput 4: 544\u2013571","journal-title":"Form Asp Comput"},{"key":"189_CR4","unstructured":"Carbonnell ER, Kapur D (2004) Program verification using automatic generation of invariants. In: Proceedings of the international conference on theoretical aspects of computing 2004, Lecture Notes in Computer Science, vol 3407. Springer Verlag, pp 325\u2013340"},{"issue":"1\u20133","key":"189_CR5","first-page":"125","volume":"80","author":"J Carette","year":"2007","unstructured":"Carette J, Janicki R (2007) Computing properties of numeric iterative programs by symbolic computation. Fundamentae Informatica 80(1\u20133): 125\u2013146","journal-title":"Fundamentae Informatica"},{"key":"189_CR6","doi-asserted-by":"crossref","unstructured":"Cheatham TE, Townley JA (1976) Symbolic evaluation of programs: a look at loop analysis. In: Proceedings of ACM symposium on symbolic and algebraic computation, pp 90\u201396","DOI":"10.1145\/800205.806327"},{"key":"189_CR7","unstructured":"Collins RW, Walton GH, Hevner AR, Linger RC (2005) The CERT function extraction experiment: quantifying FX impact on software comprehension and verification. Technical Report CMU\/SEI-2005-TN-047. Software Engineering Institute, Carnegie Mellon University"},{"key":"189_CR8","doi-asserted-by":"crossref","unstructured":"Colon MA, Sankaranarayana S, Sipma HB (2003) Linear invariant generation using non linear constraint solving. In: Proceedings of the computer aided verification. CAV 2003. Lecture Notes in Computer Science, vol 2725. Springer Verlag, pp 420\u2013432","DOI":"10.1007\/978-3-540-45069-6_39"},{"key":"189_CR9","doi-asserted-by":"crossref","unstructured":"Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings, fourth ACM symposium on principles of programming languages. Los Angeles, CA","DOI":"10.1145\/512950.512973"},{"key":"189_CR10","doi-asserted-by":"crossref","unstructured":"Cousot P, Halbwachs N (1978) Automatic discovery of linear restraints among variables of a program. In: Conference record of the fifth annual ACM SIGPLAN-SIGACT symposium on the principles of programming languages, pp 84\u201397","DOI":"10.1145\/512760.512770"},{"key":"189_CR11","doi-asserted-by":"crossref","unstructured":"Denney E, Fischer B (2006) 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","DOI":"10.1145\/1173706.1173725"},{"key":"189_CR12","volume-title":"A discipline of programming","author":"EW Dijkstra","year":"1976","unstructured":"Dijkstra EW (1976) A discipline of programming. Prentice Hall, Englewood Cliffs"},{"issue":"3","key":"189_CR13","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1109\/TSE.1984.5010236","volume":"10","author":"D Dunlop","year":"1984","unstructured":"Dunlop D, Basili VR (1984) A heuristic for deriving loop functions. IEEE Trans Softw Eng 10(3): 275\u2013285","journal-title":"IEEE Trans Softw Eng"},{"key":"189_CR14","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1016\/j.scico.2007.01.015","volume":"69","author":"MD Ernst","year":"2006","unstructured":"Ernst MD, Perkins JH, Guo PJ, McCamant S, Pacheco C, Tschantz MS, Xiao C (2006) The Daikon system for dynamic detection of likely invariants. Sci Comput Program 69: 35\u201345","journal-title":"Sci Comput Program"},{"key":"189_CR15","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-36614-8","volume-title":"Advanced symbolic analysis for compilers","author":"T Fahringer","year":"2003","unstructured":"Fahringer T, Scholz B (2003) Advanced symbolic analysis for compilers. Springer Verlag, Berlin"},{"key":"189_CR16","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 (1981) The science of programming. Springer Verlag, Berlin"},{"key":"189_CR17","unstructured":"Gulwani S, McCloskey B, Tiwari A (2008) Lifting abstract interpreters to quantified logic domains. In: 35th ACM symposium on principles of programming languages, pp 235\u2013246. ACM, January 2008"},{"key":"189_CR18","unstructured":"Hevner AR, Linger RC, Collins RW, Pleszkoch MG, Prowell SJ, Walton GH (2005) The impact of function extraction technology on next generation software engineering. Technical Report CMU\/SEI-2005-TR-015, Software Engineering Institute, July 2005"},{"issue":"10","key":"189_CR19","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare CAR (1969) An axiomatic basis for computer programming. Commun ACM 12(10): 576\u2013583","journal-title":"Commun ACM"},{"key":"189_CR20","unstructured":"Hu L, Harman M, Hierons R, Binkley D (2004) Loop squashing transformations for amorphous slicing. In: Proceedings of the 11th working conference on reverse engineering. IEEE Computer Society"},{"key":"189_CR21","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1007\/BF00268497","volume":"6","author":"M Karr","year":"1976","unstructured":"Karr M (1976) Affine relationships among variables of a program. Acta Inform 6: 133\u2013151","journal-title":"Acta Inform"},{"key":"189_CR22","unstructured":"Kovacs L, Jebelean T (2004) Automated generation of loop invariants by recurrence solving in theorema. In: Petcu D, Negru V, Zaharie D, Jebelean T (eds) Proceedings of the 6th international symposium on symbolic and numeric algorithms for scientific computing (SYNASC04). Timisoara. Romania. Mirton Publisher, pp 451\u2013464"},{"key":"189_CR23","doi-asserted-by":"crossref","unstructured":"Kovacs L, Jebelean T (2005) 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","DOI":"10.1109\/SYNASC.2005.19"},{"key":"189_CR24","unstructured":"Linger RC, Mills HD, Witt BI (1979) Structured programming. Addison Wesley, Reading"},{"key":"189_CR25","doi-asserted-by":"crossref","unstructured":"Linger RC, Pleszkoch M (2004) Improving network system security with function extraction technology for automated calculation of program behavior. In: Proceedings of the 37th annual Hawaii international conference on system science (HICSS35), Hawaii. IEEE Computer Society Press, Los Alamitos, CA","DOI":"10.1109\/HICSS.2004.1265704"},{"key":"189_CR26","doi-asserted-by":"crossref","unstructured":"Linger RC, Walton G, Hevner A, Burns L (2007) Next-generation software engineering: Function extraction for computation of software behavior. In: Proceedings of the Hawaii international conference on system sciences, HICSS-40. Kona, Hawaii. IEEE Computer Society Press, Los Alamitos, CA","DOI":"10.1109\/HICSS.2007.403"},{"key":"189_CR27","unstructured":"Louhichi A, Mraihi O, Jilani LL, Mili A (2009) Invariant assertions. invariant relations and invariant functions. In: Proceedings of the 2nd international workshop on invariant generation, York, UK"},{"key":"189_CR28","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1007\/BF01237234","volume":"28","author":"TJ Marlowe","year":"1990","unstructured":"Marlowe TJ, Ryder BG (1990) Properties of dataflow frameworks: a unified model. Acta Inform 28: 121\u2013163","journal-title":"Acta Inform"},{"key":"189_CR29","unstructured":"McCune W (2003) Otter 3.3 reference manual. Technical Report Technical Memorandum No 263, Argonne National Laboratory. August 2003"},{"key":"189_CR30","doi-asserted-by":"crossref","first-page":"989","DOI":"10.1016\/j.scico.2009.09.009","volume":"74","author":"A Mili","year":"2009","unstructured":"Mili A, Aharon S, Nadkarni Ch (2009) Mathematics for reasoning about loop. Sci Comput Program 74: 989\u20131020","journal-title":"Sci Comput Program"},{"key":"189_CR31","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1007\/BF00290145","volume":"22","author":"A Mili","year":"1985","unstructured":"Mili A, Desharnais J, Gagne JR (1985) Strongest invariant functions: Their use in the systematic analysis of while statements. Acta Inform 22: 47\u201366","journal-title":"Acta Inform"},{"issue":"3","key":"189_CR32","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1007\/BF00265990","volume":"24","author":"A Mili","year":"1987","unstructured":"Mili A, Desharnais J, Mili F (1987) Relational heuristics for the design of deterministic programs. Acta Inform 24(3): 239\u2013276","journal-title":"Acta Inform"},{"key":"189_CR33","doi-asserted-by":"crossref","first-page":"1114","DOI":"10.1016\/j.jsc.2008.11.007","volume":"45","author":"A Mili","year":"2009","unstructured":"Mili A, Aharon S, Nadkarni C, Mraihi O, Louhichi A, Jilani LL (2009) Reflexive transitive invariant relations: a basis for computing loop functions. J Symb Comput 45: 1114\u20131143","journal-title":"J Symb Comput"},{"issue":"1","key":"189_CR34","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1145\/360569.360659","volume":"18","author":"HD Mills","year":"1975","unstructured":"Mills HD (1975) The new math of computer programming. Commun ACM 18(1): 43\u201348","journal-title":"Commun ACM"},{"key":"189_CR35","doi-asserted-by":"crossref","unstructured":"Mraihi O, Louhichi A, Jilani LL, Desharnais J, Mili A (2012) Invariant assertions, invariant relations. and invariant functions. Sci Comput Program. doi: 10.1016\/j.scico.2012.05.006","DOI":"10.1016\/j.scico.2012.05.006"},{"key":"189_CR36","doi-asserted-by":"crossref","unstructured":"Pleszkoch M, Hausler P, Hevner A, Linger RC (1990) Function-theoretic principles of program understanding. In: Proceedings of the 23rd annual Hawaii international conference on system science (HICSS35), Hawaii. IEEE Computer Society Press, Los Alamitos, CA","DOI":"10.1109\/HICSS.1990.205177"},{"key":"189_CR37","doi-asserted-by":"crossref","unstructured":"Podelski A, Rybalchenko A (2004) Transition invariants. In: Proceedings of the 19th annual symposium on logic in computer science, pp 132\u2013144","DOI":"10.1109\/LICS.2004.1319598"},{"key":"189_CR38","unstructured":"Pollack W (2005) Meeting the challenge of ultra large scale (uls) systems. Technical Report http:\/\/www.sei.cmu.edu\/news-at-sei\/features\/2005\/4\/feature-2-2005-4.htm . Software Engineering Institute. Carnegie Mellon University, Pittsburgh, PA"},{"key":"189_CR39","unstructured":"Sankaranarayana S, Sipma HB, Manna Z (2004) Non linear loop invariant generation using Groebner bases. In: Proceedings, ACM SIGPLAN principles of programming languages. POPL 2004, pp 381\u2013329"},{"key":"189_CR40","volume-title":"Advanced symbolic analysis of compilers","author":"V Scholz","year":"2003","unstructured":"Scholz V, Fahringer T (2003) Advanced symbolic analysis of compilers. Springer Verlag, Berlin"},{"key":"189_CR41","unstructured":"Sharir M, Pnueli A (1981) Two approaches to inter procedural data flow analysis. In: Jones M (ed) Program flow analysis: theory and applications"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-012-0189-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11334-012-0189-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-012-0189-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,2]],"date-time":"2019-07-02T20:20:15Z","timestamp":1562098815000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11334-012-0189-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,8,14]]},"references-count":41,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2012,9]]}},"alternative-id":["189"],"URL":"https:\/\/doi.org\/10.1007\/s11334-012-0189-0","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"value":"1614-5046","type":"print"},{"value":"1614-5054","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,8,14]]}}}