{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:09:31Z","timestamp":1761610171966,"version":"build-2065373602"},"reference-count":21,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[2002,12,1]],"date-time":"2002-12-01T00:00:00Z","timestamp":1038700800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2002,12,1]],"date-time":"2002-12-01T00:00:00Z","timestamp":1038700800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":3893,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2002,12]]},"DOI":"10.1016\/s1571-0661(04)80400-6","type":"journal-article","created":{"date-parts":[[2004,9,29]],"date-time":"2004-09-29T12:47:47Z","timestamp":1096462067000},"page":"1-16","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":5,"title":["Predicate Abstraction and Refinement for Model Checking VHDL State Machines"],"prefix":"10.1016","volume":"66","author":[{"given":"Mustapha","family":"Bourahla","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mohamed","family":"Benmohamed","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)80400-6_NEWBIB1","unstructured":"C. Barret, D. Dill, and J. Levitt. Validity checking for combinations of theories with equality. In Mandayam Srivas and Albert Camilleri, editors, Formal Methods in Computer-Aided Design (FMCAD'96), volume 1196 of Lecture Notes in Computer Science, pages 187\u2013201, Palo Alto, CA, November 1996. Springer-Verlag."},{"key":"10.1016\/S1571-0661(04)80400-6_NEWBIB2","unstructured":"S. Bensalem, A. Bouajjani, C. Loiseaux, and J. Sifakis. Property preserving simulations. In CAV'92, pages 251\u2013263, 1992."},{"key":"10.1016\/S1571-0661(04)80400-6_NEWBIB3","doi-asserted-by":"crossref","unstructured":"S. Bensalem, Y. Lakhnech, and S. Owre. Computing abstractions of infinite state systems compositionally and automatically. In Hu and Vardi [HV98], pages 319\u2013331, 1998.","DOI":"10.1007\/BFb0028755"},{"key":"10.1016\/S1571-0661(04)80400-6_NEWBIB4","doi-asserted-by":"crossref","unstructured":"S. Bensalem, Y. Lakhnech, and H. Saidi. Powerful techniques for the automatic generation of invariants. In R. Alur and T.A. Henzinger, editors, 8th International Conference on Computer Aided Verification, volume 1102 of Lecture Notes in Computer Science, pages 323\u2013335. Springer\u2014Verlag, 1996.","DOI":"10.1007\/3-540-61474-5_80"},{"key":"10.1016\/S1571-0661(04)80400-6_NEWBIB5","unstructured":"T. Chaney, J.A. Fingerhut, M. Flucke, and J. Turner. Design of a gigabit ATM switching system. Technical Report WUCS-96\u201307. Computer Science Department, Washington university, St. Louis, Missouri, 1996."},{"key":"10.1016\/S1571-0661(04)80400-6_NEWBIB6","series-title":"Computer-Aided Verification, Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/10722167_15","article-title":"Counterexample-guided abstraction refinement","author":"Clarke","year":"2000"},{"issue":"5","key":"10.1016\/S1571-0661(04)80400-6_NEWBIB7","doi-asserted-by":"crossref","first-page":"1512","DOI":"10.1145\/186025.186051","article-title":"Model checking and abstraction","volume":"16","author":"Clarke","year":"1994","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"10.1016\/S1571-0661(04)80400-6_NEWBIB8","doi-asserted-by":"crossref","unstructured":"M.A. Colon and T.E. Uribe. Generating finite-state abstractions of reactive systems using decision procedures. In Hu and Vardi, pages 293\u2013304, 1998.","DOI":"10.1007\/BFb0028753"},{"key":"10.1016\/S1571-0661(04)80400-6_NEWBIB9","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In 4th ACM symp. of Prog. Lang. Pages 238\u2013252. ACM Press, 1977.","DOI":"10.1145\/512950.512973"},{"key":"10.1016\/S1571-0661(04)80400-6_NEWBIB10","unstructured":"D. Dams. Abstract interpretation and partition refinement for model checking. PhD thesis, Technical University of Eindhoven, 1996."},{"key":"10.1016\/S1571-0661(04)80400-6_NEWBIB11","series-title":"CAV'94","first-page":"455","article-title":"Model checking using adaptive state and data abstraction","author":"Dams","year":"1994"},{"key":"10.1016\/S1571-0661(04)80400-6_NEWBIB12","doi-asserted-by":"crossref","unstructured":"S. Das, D.L. Dill, and S. Park. Experience with predicate abstraction. In Halbwachs and Peled [HP99], pages 160\u2013171, 1999.","DOI":"10.1007\/3-540-48683-6_16"},{"key":"10.1016\/S1571-0661(04)80400-6_NEWBIB13","series-title":"Computer Aided Verification, volume 939 of LNCS","first-page":"54","article-title":"Model checking for infinite state systems using data abstraction","author":"Dingel","year":"1995"},{"key":"10.1016\/S1571-0661(04)80400-6_NEWBIB14","doi-asserted-by":"crossref","unstructured":"S. Graf and H. Saidi. Construction of abstract state graphs with PVS. In Computer Aided Verification, volume 1254 of Lecture Notes in Computer Science, 1997.","DOI":"10.1007\/3-540-63166-6_10"},{"year":"1994","series-title":"Computer-Aided Verification of coordinating processes","author":"Kurshan","key":"10.1016\/S1571-0661(04)80400-6_NEWBIB15"},{"key":"10.1016\/S1571-0661(04)80400-6_NEWBIB16","unstructured":"J.R. Levitt. Formal verification techniques for digital systems. PhD thesis, Stanford university, December 1998."},{"issue":"1","key":"10.1016\/S1571-0661(04)80400-6_NEWBIB17","doi-asserted-by":"crossref","DOI":"10.1007\/BF01384313","article-title":"Property preserving abstractions for the verification of concurrent systems","volume":"6","author":"Loiseaux","year":"1995","journal-title":"Formal Methods in System Design"},{"key":"10.1016\/S1571-0661(04)80400-6_NEWBIB18","unstructured":"D. E. Long. Model Checking, Abstraction and Compositional Reasoning. PhD thesis, Carnegie Mellon, 1993."},{"year":"1991","series-title":"Applications of VHDL to circuit design","author":"Harr","key":"10.1016\/S1571-0661(04)80400-6_NEWBIB19"},{"year":"1993","series-title":"Symbolic model checking","author":"McMillan","key":"10.1016\/S1571-0661(04)80400-6_NEWBIB20"},{"key":"10.1016\/S1571-0661(04)80400-6_NEWBIB21","doi-asserted-by":"crossref","unstructured":"H. Saidi and N. Shankar. Abstract and model check while you prove. In Halbwaks and Peled [HP99], pages 443\u2013454, 1999.","DOI":"10.1007\/3-540-48683-6_38"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104804006?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104804006?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:05:15Z","timestamp":1761609915000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104804006"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,12]]},"references-count":21,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2002,12]]}},"alternative-id":["S1571066104804006"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)80400-6","relation":{},"ISSN":["1571-0661"],"issn-type":[{"type":"print","value":"1571-0661"}],"subject":[],"published":{"date-parts":[[2002,12]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Predicate Abstraction and Refinement for Model Checking VHDL State Machines","name":"articletitle","label":"Article Title"},{"value":"Electronic Notes in Theoretical Computer Science","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/S1571-0661(04)80400-6","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"converted-article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 2002 Published by Elsevier B.V.","name":"copyright","label":"Copyright"}]}}