{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:28:39Z","timestamp":1767929319342,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540242970","type":"print"},{"value":"9783540305798","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-30579-8_22","type":"book-chapter","created":{"date-parts":[[2010,12,20]],"date-time":"2010-12-20T16:45:34Z","timestamp":1292863534000},"page":"330-345","source":"Crossref","is-referenced-by-count":1,"title":["Verification of an Error Correcting Code by Abstract Interpretation"],"prefix":"10.1007","author":[{"given":"Charles","family":"Hymans","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"22_CR1","unstructured":"ANSI\/IEEE Std 1076-1987. IEEE Standard VHDL Language Reference Manual (1988)"},{"key":"22_CR2","unstructured":"IEEE Std 1164-1993. IEEE Standard Multivalue Logic System for VHDL Model Interoperability, (Std_logic_1164) (1993)"},{"key":"22_CR3","unstructured":"Accellera. Property Specification Language Reference Manual, Version 1.01 (2003), http:\/\/www.accellera.org\/pslv101.pdf"},{"key":"22_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/3-540-44585-4_33","volume-title":"Computer Aided Verification","author":"I. Beer","year":"2001","unstructured":"Beer, I., Ben-David, S., Eisner, C., Fisman, D., Gringauze, A., Rodeh, Y.: The temporal logic sugar. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 363\u2013367. Springer, Heidelberg (2001)"},{"key":"22_CR5","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1145\/309847.309942","volume-title":"Proceedings of the 36th Design Automation Conference (DAC 1999)","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y.: Symbolic model checking using SAT procedure instead of BDDs. In: Proceedings of the 36th Design Automation Conference (DAC 1999), pp. 317\u2013320. ACM Press, New York (1999)"},{"key":"22_CR6","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1145\/781131.781153","volume-title":"Conference on Programming Language Design and Implementation (PLDI 2003)","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: Conference on Programming Language Design and Implementation (PLDI 2003), pp. 196\u2013207. ACM Press, New York (2003)"},{"issue":"8","key":"22_CR7","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers\u00a035(8), 677\u2013691 (1986)","journal-title":"IEEE Transactions on Computers"},{"key":"22_CR8","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1145\/123186.128296","volume-title":"Proceedings of the 27th ACM\/IEEE Design Automation Conference (DAC 1990)","author":"R.E. Bryant","year":"1990","unstructured":"Bryant, R.E.: Symbolic simulation - techniques and applications. In: Proceedings of the 27th ACM\/IEEE Design Automation Conference (DAC 1990), pp. 517\u2013521. IEEE Computer Society Press, Los Alamitos (1990)"},{"issue":"4","key":"22_CR9","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1109\/43.275352","volume":"13","author":"J.R. Burch","year":"1994","unstructured":"Burch, J.R., Clarke, E.M., Long, D.E., McMillan, K.L., Dill, D.L.: Symbolic model checking for sequential circuit verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems\u00a013(4), 401\u2013424 (1994)","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"22_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/3-540-48683-6_19","volume-title":"Computer Aided Verification","author":"C.-T. Chou","year":"1999","unstructured":"Chou, C.-T.: The mathematical foundation of symbolic trajectory evaluation. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 196\u2013207. Springer, Heidelberg (1999)"},{"key":"22_CR11","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1145\/775832.775928","volume-title":"Proceedings of the 40th Design Automation Conference (DAC 2003)","author":"E.M. Clarke","year":"2003","unstructured":"Clarke, E.M., Kroening, D., Yorav, K.: Behavioral consistency of C and verilog programs using bounded model checking. In: Proceedings of the 40th Design Automation Conference (DAC 2003), pp. 368\u2013371. ACM Press, New York (2003)"},{"key":"22_CR12","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1145\/512950.512973","volume-title":"4th ACM Symposium on Principles of Programming Languages (POPL 1977)","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: 4th ACM Symposium on Principles of Programming Languages (POPL 1977), pp. 238\u2013252. ACM Press, New York (1977)"},{"issue":"8","key":"22_CR13","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, nondeterminacy and formal derivation of programs. Communications of the ACM\u00a018(8), 453\u2013457 (1975)","journal-title":"Communications of the ACM"},{"key":"22_CR14","doi-asserted-by":"crossref","unstructured":"Granger, P.: Static analysis of linear congruence equalities among variables of a program. In: Proceedings of the International Joint Conference on Theory and Practice of Software Development (TAPSOFT 1991), vol.1 pp. 169\u2013192 (1991)","DOI":"10.1007\/3-540-53982-4_10"},{"key":"22_CR15","unstructured":"The VIS Group. Vis: A system for verification and synthesis. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 428\u2013432. Springer, Heidelberg (1996)"},{"issue":"6","key":"22_CR16","doi-asserted-by":"publisher","first-page":"679","DOI":"10.1007\/BF00282621","volume":"24","author":"S. Horwitz","year":"1987","unstructured":"Horwitz, S., Demers, A.J., Teitelbaum, T.: An efficient general iterative algorithm for dataflow analysis. Acta Informatica\u00a024(6), 679\u2013694 (1987)","journal-title":"Acta Informatica"},{"key":"22_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"444","DOI":"10.1007\/3-540-45789-5_31","volume-title":"Static Analysis","author":"C. Hymans","year":"2002","unstructured":"Hymans, C.: Checking Safety Properties of Behavioral VHDL Descriptions by Abstract Interpretation. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol.\u00a02477, pp. 444\u2013460. Springer, Heidelberg (2002)"},{"key":"22_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-540-39724-3_23","volume-title":"Correct Hardware Design and Verification Methods","author":"C. Hymans","year":"2003","unstructured":"Hymans, C.: Design and Implementation of an Abstract Interpreter for VHDL. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol.\u00a02860, pp. 263\u2013269. Springer, Heidelberg (2003)"},{"key":"22_CR19","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":"22_CR20","doi-asserted-by":"crossref","unstructured":"Kildall, G.A.: A unified approach to global program optimization. In: 1st ACM Symposium on Principles of Programming Languages (POPL 1973), pp. 194\u2013206 (1973)","DOI":"10.1145\/512927.512945"},{"key":"22_CR21","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1145\/378239.378278","volume-title":"Proceedings of the 38th Design Automation Conference (DAC 2001)","author":"A. K\u00f6lbl","year":"2001","unstructured":"K\u00f6lbl, A., Kukula, J.H., Damiano, R.F.: Symbolic RTL simulation. In: Proceedings of the 38th Design Automation Conference (DAC 2001), pp. 47\u201352. ACM Press, New York (2001)"},{"key":"22_CR22","unstructured":"Leroy, X., Doligez, D., Garrigue, J., R\u00e9my, D., Vouillon, J.: The Objective Caml System, Documentation and User\u2019s Manual. INRIA-Institut National de Recherche en Informatique et en Automatique (2002)"},{"key":"22_CR23","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":"22_CR24","unstructured":"Plotkin, G.: A structural approach to operational semantics. Technical Report DAIMI FN-19, Aarhus University (1981)"},{"key":"22_CR25","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1137\/0108018","volume":"8","author":"I.S. Reed","year":"1960","unstructured":"Reed, I.S., Solomon, G.: Polynomial codes over certain finite fields. Journal of the Society for Industrial and Applied Mathematics\u00a08, 300\u2013304 (1960)","journal-title":"Journal of the Society for Industrial and Applied Mathematics"},{"issue":"2","key":"22_CR26","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BF01383966","volume":"6","author":"C.-J.H. Seger","year":"1995","unstructured":"Seger, C.-J.H., Bryant, R.E.: Formal verification by symbolic evaluation of partially-ordered trajectories. Formal Methods in System Design\u00a06(2), 147\u2013189 (1995)","journal-title":"Formal Methods in System Design"},{"key":"22_CR27","doi-asserted-by":"crossref","unstructured":"Simon, A., King, A., Howe, J.M.: Two variables per linear inequality as an abstract domain. In: Logic Based Program Synthesis and Tranformation (LOPSTR 2002), pp. 71\u201389 (2002)","DOI":"10.1007\/3-540-45013-0_7"}],"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-540-30579-8_22.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T04:24:17Z","timestamp":1605759857000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30579-8_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540242970","9783540305798"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30579-8_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}