{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T09:14:12Z","timestamp":1673428452702},"reference-count":42,"publisher":"Elsevier BV","issue":"14","license":[{"start":{"date-parts":[[2002,11,1]],"date-time":"2002-11-01T00:00:00Z","timestamp":1036108800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Information and Software Technology"],"published-print":{"date-parts":[[2002,11]]},"DOI":"10.1016\/s0950-5849(02)00120-9","type":"journal-article","created":{"date-parts":[[2002,10,21]],"date-time":"2002-10-21T10:49:54Z","timestamp":1035197394000},"page":"857-873","source":"Crossref","is-referenced-by-count":6,"title":["Detection of dynamic execution errors in IBM system automation's rule-based expert system"],"prefix":"10.1016","volume":"44","author":[{"given":"Carsten","family":"Sinz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Lumpp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J\u00fcrgen","family":"Schneider","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wolfgang","family":"K\u00fcchlin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0950-5849(02)00120-9_BIB1","doi-asserted-by":"crossref","first-page":"447","DOI":"10.1016\/0020-7373(92)90043-K","article-title":"A Petri-net based approach for verifying the integrity of production systems","volume":"36","author":"Agarwal","year":"1992","journal-title":"Int. J. Man\u2013Machine Studies"},{"key":"10.1016\/S0950-5849(02)00120-9_BIB2","series-title":"Proceedings of AAAI Workshop on Verification and Validation of Expert Systems","volume":"July","author":"Andert","year":"1992"},{"key":"10.1016\/S0950-5849(02)00120-9_BIB3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-49059-0_14","article-title":"Symbolic model checking without BDDs","volume":"vol. 1579","author":"Biere","year":"1999"},{"issue":"4","key":"10.1016\/S0950-5849(02)00120-9_BIB4","doi-asserted-by":"crossref","first-page":"34","DOI":"10.1109\/52.391826","article-title":"Seven more myths of formal methods","volume":"12","author":"Bowen","year":"1995","journal-title":"IEEE Soft."},{"issue":"3","key":"10.1016\/S0950-5849(02)00120-9_BIB5","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/136035.136043","article-title":"Symbolic boolean manipulation with ordered binary-decision diagrams","volume":"24","author":"Bryant","year":"1992","journal-title":"ACM Comput. Surv."},{"issue":"2","key":"10.1016\/S0950-5849(02)00120-9_BIB6","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1109\/32.345825","article-title":"Formal methods reality check: Industrial usage","volume":"21","author":"Craigen","year":"1995","journal-title":"IEEE Trans. Soft. Engng"},{"issue":"2","key":"10.1016\/S0950-5849(02)00120-9_BIB7","first-page":"34","article-title":"Can formal methods always deliver?","volume":"30","author":"Fenton","year":"1997","journal-title":"IEEE Comput."},{"issue":"3","key":"10.1016\/S0950-5849(02)00120-9_BIB8","first-page":"203","article-title":"Applying formal verification methods to rule-based programs","volume":"7","author":"Gamble","year":"1994","journal-title":"Int. J. Expert Syst."},{"key":"10.1016\/S0950-5849(02)00120-9_BIB9","unstructured":"S. Garone, N. Buck, Capturing, reusing, and applying knowledge for competitive advantage: computer associate's aion. International Data Corporation, 2000. IDC White Paper."},{"issue":"1\/2","key":"10.1016\/S0950-5849(02)00120-9_BIB10","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1016\/S0019-9958(85)80014-0","article-title":"A proof rule for fair termination of guarded commands","volume":"66","author":"Grumberg","year":"1985","journal-title":"Inform. Control"},{"issue":"5","key":"10.1016\/S0950-5849(02)00120-9_BIB11","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1109\/52.57887","article-title":"Seven myths of formal methods","volume":"7","author":"Hall","year":"1990","journal-title":"IEEE Soft."},{"key":"10.1016\/S0950-5849(02)00120-9_BIB12","series-title":"Extensions of Classical Logic","first-page":"507","article-title":"Dynamic logic","volume":"vol. II","author":"Harel","year":"1984"},{"issue":"1\u20133","key":"10.1016\/S0950-5849(02)00120-9_BIB13","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1016\/S0019-9958(82)90553-8","article-title":"Looping vs. repeating in dynamic logic","volume":"55","author":"Harel","year":"1982","journal-title":"Inform. Control"},{"issue":"9","key":"10.1016\/S0950-5849(02)00120-9_BIB14","doi-asserted-by":"crossref","first-page":"921","DOI":"10.1145\/4284.4286","article-title":"Rule based systems","volume":"28","author":"Hayes-Roth","year":"1985","journal-title":"Commun. ACM"},{"key":"10.1016\/S0950-5849(02)00120-9_BIB15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-48118-4_59","article-title":"Formal specification of a voice communication system used in air traffic control: an industrial application of light-weight formal methods using VDM++","volume":"vol. 1249","author":"H\u00f6rl","year":"1999"},{"key":"10.1016\/S0950-5849(02)00120-9_BIB16","unstructured":"A. Kaiser, A SAT-based propositional prover for consistency checking of automotive product data. Technical report, Wilhelm-Schickard-Instimt f\u00fcr Informatik, Eberhard-Karls-Universit\u00e4t T\u00fcbingen, Sand 13, 72076 T\u00fcbingen, Germany, 2001. Technical Report WSI-2001-16."},{"key":"10.1016\/S0950-5849(02)00120-9_BIB17","article-title":"Explaining inconsistencies in combinatorial automotive product data","volume":"November","author":"Kaiser","year":"2001"},{"key":"10.1016\/S0950-5849(02)00120-9_BIB18","article-title":"Encoding plans in propositional logic","volume":"November","author":"Kautz","year":"1996"},{"key":"10.1016\/S0950-5849(02)00120-9_BIB19","article-title":"Planning as satisfiability","author":"Kautz","year":"1992"},{"issue":"1 and 2","key":"10.1016\/S0950-5849(02)00120-9_BIB20","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1023\/A:1006370506164","article-title":"Proving consistency assertions for automotive product data management","volume":"24","author":"K\u00fcchlin","year":"2000","journal-title":"J. Autom. Reason., (Special Issue: Satisfiability in the Year 2000)"},{"key":"10.1016\/S0950-5849(02)00120-9_BIB21","doi-asserted-by":"crossref","DOI":"10.1145\/378239.379017","article-title":"Chaff: Engineering an efficient SAT solver","author":"Moskewicz","year":"2001"},{"key":"10.1016\/S0950-5849(02)00120-9_BIB22","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1016\/S0020-7373(89)80002-1","article-title":"Issues in the verification of knowledge in rule-based systems","volume":"30","author":"Nazareth","year":"1989","journal-title":"Int. J. Man\u2013Mach. Stud."},{"issue":"3","key":"10.1016\/S0950-5849(02)00120-9_BIB23","doi-asserted-by":"crossref","first-page":"402","DOI":"10.1109\/69.224193","article-title":"Investigating the applicability of Petri nets for rule-based system verification","volume":"4","author":"Nazareth","year":"1993","journal-title":"IEEE Trans. Knowledge Data Engng"},{"key":"10.1016\/S0950-5849(02)00120-9_BIB24","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1016\/S1042-8143(05)80024-X","article-title":"Verification of rule-based knowledge using directed graphs","volume":"3","author":"Nazareth","year":"1991","journal-title":"Knowledge Acquisition"},{"issue":"2","key":"10.1016\/S0950-5849(02)00120-9_BIB25","first-page":"69","article-title":"Checking a knowledge-based system for consistency and completeness\/knowledge base verification","volume":"8","author":"Nguyen","year":"1987","journal-title":"AI Magazine"},{"issue":"2","key":"10.1016\/S0950-5849(02)00120-9_BIB26","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1109\/2.566148","article-title":"Investigating the influence of formal methods","volume":"30","author":"Pfleeger","year":"1997","journal-title":"IEEE Computer"},{"issue":"2","key":"10.1016\/S0950-5849(02)00120-9_BIB27","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1006\/ijhc.1996.0008","article-title":"Validating dynamic properties of rule-based systems","volume":"44","author":"Preece","year":"1996","journal-title":"Int. J. Human\u2013Comp. Stud."},{"issue":"2","key":"10.1016\/S0950-5849(02)00120-9_BIB28","article-title":"Using directed hypergraphs to verify rule-based expert systems","volume":"9","author":"Ramaswamy","year":"1997","journal-title":"IEEE Trans. Knowledge Data Engng"},{"key":"10.1016\/S0950-5849(02)00120-9_BIB29","article-title":"A theoretical basis for the assessment of rule-based system reliability","volume":"July","author":"Shaft","year":"2000","journal-title":"Found. Inform. Syst."},{"key":"10.1016\/S0950-5849(02)00120-9_BIB30","series-title":"Electronic Notes in Discrete Mathematics, Boston, MA","article-title":"PaSAT\u2014parallel SAT-checking with lemma exchange: implementation and applications","volume":"vol. 9","author":"Sinz","year":"2001"},{"key":"10.1016\/S0950-5849(02)00120-9_BIB31","series-title":"Proceedings of 14th International FLAIRS Conference, Key West, FL","first-page":"645","article-title":"Detection of inconsistencies in complex product model data using extended propositional SAT-checking","author":"Sinz","year":"2001"},{"key":"10.1016\/S0950-5849(02)00120-9_BIB32","series-title":"Proceedings of the 2nd Asia\u2013Pacific Conference on Quality Software (APAQS 2001), Hong Kong","author":"Sinz","year":"2001"},{"key":"10.1016\/S0950-5849(02)00120-9_BIB33","unstructured":"F. Somenzi, CUDD: CU Decision Diagram Package, Release 2.3.0. University of Colorado, Boulder, 1998. Available at http:\/\/vlsi.colorado.edu\/~fabio."},{"key":"10.1016\/S0950-5849(02)00120-9_BIB34","series-title":"International Computer Science Series","author":"Sommerville","year":"1997"},{"key":"10.1016\/S0950-5849(02)00120-9_BIB35","series-title":"ECAI 2000, 14th European Conference on Artificial Intelligence","volume":"vol. 10","author":"Spreeuwenberg","year":"2000"},{"key":"10.1016\/S0950-5849(02)00120-9_BIB36","unstructured":"The Standish Group International, Inc. Five \u201cT's\u201d of Data Base Availability, 1999. http:\/\/www.pm2go.com\/sample_research\/FiveTs.pdf."},{"issue":"1\/2","key":"10.1016\/S0950-5849(02)00120-9_BIB37","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1016\/S0019-9958(82)91258-X","article-title":"Propositional dynamic logic of looping and converse is elementarily decidable","volume":"54","author":"Streett","year":"1982","journal-title":"Inform. Control"},{"key":"10.1016\/S0950-5849(02)00120-9_BIB38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0016843","article-title":"Ordered binary decision diagrams and the Davis\u2013Putnam procedure","volume":"vol. 845","author":"Uribe","year":"1994"},{"key":"10.1016\/S0950-5849(02)00120-9_BIB39","unstructured":"J. van Benthem, Modal Correspondence Theory, PhD Thesis, Institut voor Logica en Grondslagenonderzoek van Exacte Wetenschappen, University of Amsterdam, 1976."},{"key":"10.1016\/S0950-5849(02)00120-9_BIB40","series-title":"Extensions of Classical Logic","first-page":"167","article-title":"Correspondence theory","volume":"vol. II","author":"van Benthem","year":"1984"},{"issue":"1","key":"10.1016\/S0950-5849(02)00120-9_BIB41","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1142\/S0218194092000075","article-title":"Proving properties of rule based systems","volume":"2","author":"Waldinger","year":"1992","journal-title":"Int. J. Soft. Engng Knowledge Engng"},{"key":"10.1016\/S0950-5849(02)00120-9_BIB42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-63104-6_28","article-title":"An efficient propositional prover","volume":"vol. 1249","author":"Zhang","year":"1997"}],"container-title":["Information and Software Technology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0950584902001209?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0950584902001209?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,9]],"date-time":"2019-04-09T06:00:35Z","timestamp":1554789635000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0950584902001209"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,11]]},"references-count":42,"journal-issue":{"issue":"14","published-print":{"date-parts":[[2002,11]]}},"alternative-id":["S0950584902001209"],"URL":"https:\/\/doi.org\/10.1016\/s0950-5849(02)00120-9","relation":{},"ISSN":["0950-5849"],"issn-type":[{"value":"0950-5849","type":"print"}],"subject":[],"published":{"date-parts":[[2002,11]]}}}