{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T06:08:32Z","timestamp":1725516512914},"publisher-location":"Berlin, Heidelberg","reference-count":39,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540691471"},{"type":"electronic","value":"9783540691495"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-69149-5_21","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T16:07:43Z","timestamp":1218557263000},"page":"189-201","source":"Crossref","is-referenced-by-count":8,"title":["The Verification Grand Challenge and Abstract Interpretation"],"prefix":"10.1007","author":[{"given":"Patrick","family":"Cousot","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"21_CR1","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: The Astr\u00e9e Static Analyzer, http:\/\/www.astree.ens.fr\/"},{"key":"21_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/3-540-36377-7_5","volume-title":"The Essence of Computation","author":"B. Blanchet","year":"2002","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In: Mogensen, T.\u00c6., Schmidt, D.A., Sudborough, I.H. (eds.) The Essence of Computation. LNCS, vol.\u00a02566, pp. 85\u2013108. Springer, Heidelberg (2002)"},{"key":"21_CR3","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1145\/781131.781153","volume-title":"Proceedings of the ACM SIGPLAN \u20192003 Conference on Programming Language Design and Implementation (PLDI)","author":"B. Blanchet","year":"2003","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: Proceedings of the ACM SIGPLAN \u20192003 Conference on Programming Language Design and Implementation (PLDI), San Diego, California, United States, June 7-14, 2003, pp. 196\u2013207. ACM Press, New York (2003)"},{"key":"21_CR4","unstructured":"Cousot, P.: M\u00e9thodes it\u00e9ratives de construction et d\u2019approximation de points fixes d\u2019op\u00e9rateurs monotones sur un treillis, analyse s\u00e9mantique de programmes (in French). In: Th\u00e8se d\u2019\u00c9tat \u00e8s sciences math\u00e9matiques, Universit\u00e9 scientifique et m\u00e9dicale de Grenoble, Grenoble, France, March 21, (1978)"},{"key":"21_CR5","first-page":"316","volume-title":"Conference Record of the Twentyfourth Annual ACM SIGPLAN--SIGACT Symposium on Principles of Programming Languages","author":"P. Cousot","year":"1997","unstructured":"Cousot, P.: Types as abstract interpretations. In: Conference Record of the Twentyfourth Annual ACM SIGPLAN--SIGACT Symposium on Principles of Programming Languages, Paris, France, January 1997, pp. 316\u2013331. ACM Press, New York (1997)"},{"key":"21_CR6","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44914-0_1","volume-title":"Abstraction, Reformulation, and Approximation","author":"P. Cousot","year":"2000","unstructured":"Cousot, P.: Partial completeness of abstract fixpoint checking. In: Choueiry, B.Y., Walsh, T. (eds.) SARA 2000. LNCS (LNAI), vol.\u00a01864, pp. 1\u201325. Springer, Heidelberg (2000)"},{"issue":"1\u20142","key":"21_CR7","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/S0304-3975(00)00313-3","volume":"277","author":"P. Cousot","year":"2002","unstructured":"Cousot, P.: Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Theoretical Computer Science\u00a0277(1\u20142), 47\u2013103 (2002)","journal-title":"Theoretical Computer Science"},{"key":"21_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/11575467_10","volume-title":"Programming Languages and Systems","author":"P. Cousot","year":"2005","unstructured":"Cousot, P.: Integrating physical systems in the static analysis of embedded control software. In: Yi, K. (ed.) APLAS 2005. LNCS, vol.\u00a03780, pp. 135\u2013138. Springer, Heidelberg (2005)"},{"key":"21_CR9","first-page":"106","volume-title":"Proceedings of the Second International Symposium on Programming","author":"P. Cousot","year":"1976","unstructured":"Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Proceedings of the Second International Symposium on Programming, Paris, France, pp. 106\u2013130. Dunod, Paris, France (1976)"},{"key":"21_CR10","series-title":"United States","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1145\/512950.512973","volume-title":"Conference Record of the Fourth Annual ACM SIGPLAN--SIGACT Symposium on Principles of Programming Languages","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the Fourth Annual ACM SIGPLAN--SIGACT Symposium on Principles of Programming Languages, Los Angeles, California. United States, pp. 238\u2013252. ACM Press, New York (1977)"},{"key":"21_CR11","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1145\/567752.567778","volume-title":"Conference Record of the Sixth Annual ACM SIGPLAN--SIGACT Symposium on Principles of Programming Languages","author":"P. Cousot","year":"1979","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Conference Record of the Sixth Annual ACM SIGPLAN--SIGACT Symposium on Principles of Programming Languages, San Antonio, Texas, pp. 269\u2013282. ACM Press, New York (1979)"},{"key":"21_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/3-540-55844-6_142","volume-title":"Programming Language Implementation and Logic Programming","author":"P. Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Comparing the Galois connection and widening\/narrowing approaches to abstract interpretation. In: Bruynooghe, M., Wirsing, M. (eds.) PLILP 1992. LNCS, vol.\u00a0631, pp. 269\u2013295. Springer, Heidelberg (1992)"},{"key":"21_CR13","first-page":"12","volume-title":"Conference Record of the Twentyseventh Annual ACM SIGPLAN--SIGACT Symposium on Principles of Programming Languages","author":"P. Cousot","year":"2000","unstructured":"Cousot, P., Cousot, R.: Temporal abstract interpretation. In: Conference Record of the Twentyseventh Annual ACM SIGPLAN--SIGACT Symposium on Principles of Programming Languages, Boston, Massachusetts, United States, January 2000, pp. 12\u201325. ACM Press, New York (2000)"},{"key":"21_CR14","first-page":"178","volume-title":"Conference Record of the Twentyninth Annual ACM SIGPLAN--SIGACT Symposium on Principles of Programming Languages","author":"P. Cousot","year":"2002","unstructured":"Cousot, P., Cousot, R.: Systematic design of program transformation frameworks by abstract interrpetation. In: Conference Record of the Twentyninth Annual ACM SIGPLAN--SIGACT Symposium on Principles of Programming Languages, Portland, Oregon, United States, January 2002, pp. 178\u2013190. ACM Press, New York (2002)"},{"key":"21_CR15","first-page":"173","volume-title":"Conference Record of the Thirtyfirst Annual ACM SIGPLAN--SIGACT Symposium on Principles of Programming Languages","author":"P. Cousot","year":"2004","unstructured":"Cousot, P., Cousot, R.: An abstract interpretation-based framework for software watermarking. In: Conference Record of the Thirtyfirst Annual ACM SIGPLAN--SIGACT Symposium on Principles of Programming Languages, Venice, Italy, January 14\u201316, 2004, pp. 173\u2013185. ACM Press, New York (2004)"},{"key":"21_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-540-71322-7_9","volume-title":"Program Analysis and Compilation, Theory and Practice","author":"P. Cousot","year":"2007","unstructured":"Cousot, P., Cousot, R.: Grammar analysis and parsing by abstract interpretation. In: Reps, T., Sagiv, M., Bauer, J. (eds.) Program Analysis and Compilation, Theory and Practice. LNCS, vol.\u00a04444, pp. 175\u2013200. Springer, Heidelberg (2007)"},{"key":"21_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-540-31987-0_3","volume-title":"Programming Languages and Systems","author":"P. Cousot","year":"2005","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: The Astr\u00e9e analyser. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 21\u201330. Springer, Heidelberg (2005)"},{"key":"21_CR18","series-title":"Lecture Notes in Computer Science","first-page":"6","volume-title":"Eleventh Annual Asian Computing Science Conference, ASIAN 06","author":"P. Cousot","year":"2006","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: Combination of abstractions in the Astr\u00e9e static analyzer. In: Okada, M., Satoh, I. (eds.) Eleventh Annual Asian Computing Science Conference, ASIAN 06, LNCS, Tokyo, Japan, December 6\u20138, 2006. pp. 6\u20138. Springer, Berlin (to appear, 2006)"},{"key":"21_CR19","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1145\/512760.512770","volume-title":"Conference Record of the Fifth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"P. Cousot","year":"1978","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Conference Record of the Fifth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Tucson, Arizona, pp. 84\u201397. ACM Press, New York (1978)"},{"key":"21_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-540-24725-8_4","volume-title":"Programming Languages and Systems","author":"J. Feret","year":"2004","unstructured":"Feret, J.: Static analysis of digital filters. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol.\u00a02986, pp. 33\u201348. Springer, Heidelberg (2004)"},{"key":"21_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/978-3-540-30579-8_3","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"J. Feret","year":"2005","unstructured":"Feret, J.: The arithmetic-geometric progression abstract domain. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 42\u201358. Springer, Heidelberg (2005)"},{"issue":"1","key":"21_CR22","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1145\/602382.602403","volume":"50","author":"C.A.R. Hoare","year":"2003","unstructured":"Hoare, C.A.R.: The verifying compiler, a grand challenge for computing research. Journal of the Association for Computing Machinary\u00a050(1), 63\u201369 (2003)","journal-title":"Journal of the Association for Computing Machinary"},{"key":"21_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/978-3-540-30579-8_5","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"C.A.R. Hoare","year":"2005","unstructured":"Hoare, C.A.R.: The verifying compiler, a grand challenge for computing research. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, p. 78. Springer, Heidelberg (2005)"},{"key":"21_CR24","doi-asserted-by":"crossref","first-page":"42","DOI":"10.1145\/1111037.1111042","volume-title":"Conference Record of the Thirtythird Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"X. Leroy","year":"2006","unstructured":"Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: Conference Record of the Thirtythird Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Charleston, South Carolina, pp. 42\u201354. ACM Press, New York (2006)"},{"key":"21_CR25","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/978-1-4020-8157-6_30","volume-title":"Building the Information Society","author":"L. Mauborgne","year":"2004","unstructured":"Mauborgne, L.: Astr\u00e9e: Verification of absence of run-time error. In: Jacquart, P. (ed.) Building the Information Society, ch.\u00a04, pp. 385\u2013392. Kluwer Academic Publishers, Dordrecht (2004)"},{"key":"21_CR26","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 analyzer. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 5\u201320. Springer, Heidelberg (2005)"},{"key":"21_CR27","unstructured":"Min\u00e9, A.: The Octagon abstract domain library. http:\/\/www.di.ens.fr\/~mine\/oct\/"},{"key":"21_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/3-540-44978-7_10","volume-title":"Programs as Data Objects","author":"A. Min\u00e9","year":"2001","unstructured":"Min\u00e9, A.: A new numerical abstract domain based on difference-bound matrices. In: Danvy, O., Filinski, A. (eds.) PADO 2001. LNCS, vol.\u00a02053, pp. 155\u2013172. Springer, Heidelberg (2001)"},{"key":"21_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/3-540-45789-5_11","volume-title":"Static Analysis","author":"A. Min\u00e9","year":"2002","unstructured":"Min\u00e9, A.: A few graph-based relational numerical abstract domains. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol.\u00a02477, pp. 117\u2013132. Springer, Heidelberg (2002)"},{"key":"21_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-540-24725-8_2","volume-title":"Programming Languages and Systems","author":"A. Min\u00e9","year":"2004","unstructured":"Min\u00e9, A.: Relational abstract domains for the detection of floating-point run-time errors. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol.\u00a02986, pp. 3\u201317. Springer, Heidelberg (2004)"},{"key":"21_CR31","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1145\/1134650.1134659","volume-title":"Proceedings of the ACM SIGPLAN\/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems, LCTES \u20192006","author":"A. Min\u00e9","year":"2006","unstructured":"Min\u00e9, A.: Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics. In: Proceedings of the ACM SIGPLAN\/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems, LCTES \u20192006, June 2006, pp. 54\u201363. ACM Press, New York (2006)"},{"key":"21_CR32","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 and Symbolic Computation\u00a019, 31\u2013100 (2006)","journal-title":"Higher-Order and Symbolic Computation"},{"key":"21_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/11609773_23","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Min\u00e9","year":"2005","unstructured":"Min\u00e9, A.: Symbolic methods to enhance the precision of numerical abstract domains. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 348\u2013363. Springer, Heidelberg (2005)"},{"key":"21_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/11575467_7","volume-title":"Programming Languages and Systems","author":"D. Monniaux","year":"2005","unstructured":"Monniaux, D.: The parallel implementation of the Astr\u00e9e static analyzer. In: Yi, K. (ed.) APLAS 2005. LNCS, vol.\u00a03780, pp. 86\u201396. Springer, Heidelberg (2005)"},{"key":"21_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/3-540-36384-X_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"X. Rival","year":"2002","unstructured":"Rival, X.: Abstract interpretation based certification of assembly code. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol.\u00a02575, pp. 41\u201355. Springer, Heidelberg (2002)"},{"issue":"1","key":"21_CR36","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/s10009-003-0125-6","volume":"6","author":"X. Rival","year":"2004","unstructured":"Rival, X.: Invariant translation-based certification of assembly code. International Journal on Software and Tools for Technology Transfer\u00a06(1), 15\u201337 (2004)","journal-title":"International Journal on Software and Tools for Technology Transfer"},{"key":"21_CR37","first-page":"1","volume-title":"Conference Record of the Thirtyfirst Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"X. Rival","year":"2004","unstructured":"Rival, X.: Symbolic transfer functions-based approaches to certified compilation. In: Conference Record of the Thirtyfirst Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Venice, Italy, pp. 1\u201313. ACM Press, New York (2004)"},{"key":"21_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/11575467_23","volume-title":"Programming Languages and Systems","author":"X. Rival","year":"2005","unstructured":"Rival, X.: Abstract dependences for alarm diagnosis. In: Yi, K. (ed.) APLAS 2005. LNCS, vol.\u00a03780, pp. 347\u2013363. Springer, Heidelberg (2005)"},{"key":"21_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/11547662_21","volume-title":"Static Analysis","author":"X. Rival","year":"2005","unstructured":"Rival, X.: Understanding the origin of alarms in Astr\u00e9e. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol.\u00a03672, pp. 303\u2013319. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69149-5_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,9,14]],"date-time":"2021-09-14T17:50:30Z","timestamp":1631641830000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69149-5_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540691471","9783540691495"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69149-5_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}