{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T09:17:55Z","timestamp":1725700675680},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642327582"},{"type":"electronic","value":"9783642327599"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"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":[[2012]]},"DOI":"10.1007\/978-3-642-32759-9_7","type":"book-chapter","created":{"date-parts":[[2012,8,21]],"date-time":"2012-08-21T10:12:30Z","timestamp":1345543950000},"page":"37-51","source":"Crossref","is-referenced-by-count":2,"title":["Maximal and Compositional Pattern-Based Loop Invariants"],"prefix":"10.1007","author":[{"given":"Virginia","family":"Aponte","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierre","family":"Courtieu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yannick","family":"Moy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marc","family":"Sango","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"7_CR1","unstructured":"Aponte, V., Courtieu, P., Moy, Y., Sango, M.: Maximal and Compositional Pattern-Based Loop Invariants - Definitions and Proofs. Technical Report CEDRIC-12-2555, CEDRIC laboratory, CNAM-Paris, France (2011), \n                  \n                    http:\/\/cedric.cnam.fr\/fichiers\/art_2555.pdf"},{"key":"7_CR2","volume-title":"High Integrity Software: The SPARK Approach to Safety and Security","author":"J. Barnes","year":"2003","unstructured":"Barnes, J.: High Integrity Software: The SPARK Approach to Safety and Security. Addison-Wesley Longman Publishing Co., Inc., Boston (2003)"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Path invariants. In: Proceedings of the 2007 ACM SIGPLAN Conference on Programming language Design and Implementation, PLDI 2007, pp. 300\u2013309. ACM, New York (2007)","DOI":"10.1145\/1250734.1250769"},{"key":"7_CR4","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/s00165-008-0080-9","volume":"20","author":"A. Bradley","year":"2008","unstructured":"Bradley, A., Manna, Z.: Property-directed incremental invariant generation. Formal Aspects of Computing\u00a020, 379\u2013405 (2008), doi:10.1007\/s00165-008-0080-9","journal-title":"Formal Aspects of Computing"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/978-3-540-45069-6_39","volume-title":"Computer Aided Verification","author":"M.A. Col\u00f3n","year":"2003","unstructured":"Col\u00f3n, M.A., Sankaranarayanan, 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":"7_CR6","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proceedings of the 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL 1978, pp. 84\u201396. ACM, New York (1978)","DOI":"10.1145\/512760.512770"},{"issue":"4","key":"7_CR7","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1145\/115372.115320","volume":"13","author":"R. Cytron","year":"1991","unstructured":"Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficiently computing static single assignment form and the control dependence graph. ACM Trans. Program. Lang. Syst.\u00a013(4), 451\u2013490 (1991)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"7_CR8","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 5th International Conference on Generative Programming and Component Engineering, GPCE 2006, pp. 121\u2013130. ACM, New York (2006)","DOI":"10.1145\/1173706.1173725"},{"issue":"8","key":"7_CR9","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, non-determinacy and formal derivation of programs. Comm. ACM\u00a018(8), 453\u2013457 (1975)","journal-title":"Comm. ACM"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"Dijkstra, E.W., Scholten, C.S.: Predicate calculus and program semantics. Springer (1990)","DOI":"10.1007\/978-1-4612-3228-5"},{"key":"7_CR11","unstructured":"Verifier, E.C.: \n                  \n                    http:\/\/www.eschertech.com\/products\/ecv.php\n                  \n                  \n                 (2012)"},{"key":"7_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of Abstract State Graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"7_CR13","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1145\/1328438.1328468","volume-title":"Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008","author":"S. Gulwani","year":"2008","unstructured":"Gulwani, S., McCloskey, B., Tiwari, A.: Lifting abstract interpreters to quantified logical domains. In: Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, pp. 235\u2013246. ACM, New York (2008)"},{"key":"7_CR14","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1145\/1375581.1375623","volume-title":"Proceedings of the 2008 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2008","author":"N. Halbwachs","year":"2008","unstructured":"Halbwachs, N., P\u00e9ron, M.: Discovering properties about arrays in simple programs. In: Proceedings of the 2008 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2008, pp. 339\u2013348. ACM, New York (2008)"},{"key":"7_CR15","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1145\/1706299.1706309","volume-title":"Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010","author":"W.R. Harris","year":"2010","unstructured":"Harris, W.R., Sankaranarayanan, S., Ivan\u010di\u0107, F., Gupta, A.: Program analysis via satisfiability modulo path programs. In: Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, pp. 71\u201382. ACM, New York (2010)"},{"key":"7_CR16","unstructured":"Hi-Lite: Simplifying the use of formal methods, \n                  \n                    http:\/\/www.open-do.org\/projects\/hi-lite\/"},{"key":"7_CR17","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM\u00a012, 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/978-3-540-79709-8_35","volume-title":"Computer Science \u2013 Theory and Applications","author":"L. Kov\u00e1cs","year":"2008","unstructured":"Kov\u00e1cs, L.: Invariant Generation for P-Solvable Loops with Assignments. In: Hirsch, E.A., Razborov, A.A., Semenov, A., Slissenko, A. (eds.) CSR 2008. LNCS, vol.\u00a05010, pp. 349\u2013359. Springer, Heidelberg (2008)"},{"key":"7_CR19","volume-title":"Proceedings of the 2009 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing. SYNASC 2009","author":"L. Kov\u00e1cs","year":"2009","unstructured":"Kov\u00e1cs, L., Voronkov, A.: Finding loop invariants for programs over arrays using a theorem prover. In: Proceedings of the 2009 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing. SYNASC 2009, IEEE Computer Society, Washington, DC (2009)"},{"key":"7_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-3-540-31987-0_2","volume-title":"Programming Languages and Systems","author":"L. Mauborgne","year":"2005","unstructured":"Mauborgne, L., Rival, X.: Trace Partitioning in Abstract Interpretation Based Static Analyzers. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 5\u201320. Springer, Heidelberg (2005)"},{"key":"7_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)"},{"key":"7_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 1\u201313. Springer, Heidelberg (2003)"},{"key":"7_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/11817963_14","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2006","unstructured":"McMillan, K.L.: Lazy Abstraction with Interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 123\u2013136. Springer, Heidelberg (2006)"},{"key":"7_CR24","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A. Min\u00e9","year":"2006","unstructured":"Min\u00e9, A.: The octagon abstract domain. Higher Order Symbol. Comput.\u00a019, 31\u2013100 (2006)","journal-title":"Higher Order Symbol. Comput."},{"key":"7_CR25","volume-title":"Semantics with Applications: a formal introduction","author":"H.R. Nielson","year":"1992","unstructured":"Nielson, H.R., Nielson, F.: Semantics with Applications: a formal introduction. John Wiley & Sons, Inc., New York (1992)"},{"key":"7_CR26","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1145\/93542.93578","volume-title":"Proceedings of the ACM SIGPLAN 1990 Conference on Programming Language Design and Implementation, PLDI 1990","author":"K.J. Ottenstein","year":"1990","unstructured":"Ottenstein, K.J., Ballance, R.A., MacCabe, A.B.: The program dependence web: a representation supporting control-, data-, and demand-driven interpretation of imperative languages. In: Proceedings of the ACM SIGPLAN 1990 Conference on Programming Language Design and Implementation, PLDI 1990, pp. 257\u2013271. ACM, New York (1990)"},{"key":"7_CR27","unstructured":"RTCA. Formal methods supplement to DO-178C and DO-278A. Document RTCA DO-333, RTCA (December 2011)"},{"key":"7_CR28","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1145\/964001.964028","volume-title":"Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004","author":"S. Sankaranarayanan","year":"2004","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Non-linear loop invariant generation using Gr\u00f6bner bases. In: Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, pp. 318\u2013329. ACM, New York (2004)"},{"key":"7_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"703","DOI":"10.1007\/978-3-642-22110-1_57","volume-title":"Computer Aided Verification","author":"R. Sharma","year":"2011","unstructured":"Sharma, R., Dillig, I., Dillig, T., Aiken, A.: Simplifying Loop Invariant Generation Using Splitter Predicates. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 703\u2013719. Springer, Heidelberg (2011)"},{"key":"7_CR30","unstructured":"SPARK Pro (2012), \n                  \n                    http:\/\/www.adacore.com\/home\/products\/sparkpro\/"}],"container-title":["Lecture Notes in Computer Science","FM 2012: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-32759-9_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T01:11:54Z","timestamp":1558314714000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-32759-9_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642327582","9783642327599"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-32759-9_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}