{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,9]],"date-time":"2023-09-09T14:40:45Z","timestamp":1694270445115},"reference-count":14,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[2005,3,1]],"date-time":"2005-03-01T00:00:00Z","timestamp":1109635200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":3072,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2005,3]]},"DOI":"10.1016\/j.entcs.2004.12.021","type":"journal-article","created":{"date-parts":[[2005,3,11]],"date-time":"2005-03-11T12:26:46Z","timestamp":1110544006000},"page":"3-16","source":"Crossref","is-referenced-by-count":14,"title":["SAT-based Induction for Temporal Safety Properties"],"prefix":"10.1016","volume":"119","author":[{"given":"Roy","family":"Armoni","sequence":"first","affiliation":[]},{"given":"Limor","family":"Fix","sequence":"additional","affiliation":[]},{"given":"Ranan","family":"Fraer","sequence":"additional","affiliation":[]},{"given":"Scott","family":"Huddleston","sequence":"additional","affiliation":[]},{"given":"Nir","family":"Piterman","sequence":"additional","affiliation":[]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.entcs.2004.12.021_bib001","doi-asserted-by":"crossref","unstructured":"Beer, I., S. Ben-David, C. Eisner and A. Landver, RuleBase: An industry-oriented formal verification tool, in: Proc. 33rd Conference on Design Automation (1996), pp. 655\u2013660","DOI":"10.1145\/240518.240642"},{"key":"10.1016\/j.entcs.2004.12.021_bib002","doi-asserted-by":"crossref","unstructured":"Biere, A., A. Cimatti, E. Clarke, M. Fujita and Y. Zhu, Symbolic model checking using SAT procedures instead of BDDs, in: Proc. 36th Design Automation Conference (1999), pp. 317\u2013320","DOI":"10.1109\/DAC.1999.781333"},{"key":"10.1016\/j.entcs.2004.12.021_bib003","series-title":"Computer Aided Verification, Proc. 11th International Conference","first-page":"172","article-title":"Verifying safety properties of a PowerPC[tm] microprocessor using symbolic model checking without BDDs","volume":"1633","author":"Biere","year":"1999"},{"key":"10.1016\/j.entcs.2004.12.021_bib004","doi-asserted-by":"crossref","DOI":"10.1109\/TC.1986.1676819","article-title":"Graph-based algorithms for boolean-function manipulation","volume":"C-35","author":"Bryant","year":"1986","journal-title":"IEEE Trans. on Computers"},{"key":"10.1016\/j.entcs.2004.12.021_bib005","unstructured":"Claessen, K., Induction and state machines (1999), unpublished"},{"key":"10.1016\/j.entcs.2004.12.021_bib006","series-title":"Model Checking","author":"Clarke","year":"1999"},{"key":"10.1016\/j.entcs.2004.12.021_bib007","series-title":"Computer Aided Verification, Proc. 13th International Conference","first-page":"436","article-title":"Benefits of bounded model checking at an industrial setting","volume":"2102","author":"Copty","year":"2001"},{"key":"10.1016\/j.entcs.2004.12.021_bib008","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1023\/A:1011254632723","article-title":"Model checking of safety properties","volume":"19","author":"Kupferman","year":"2001","journal-title":"Formal methods in System Design"},{"key":"10.1016\/j.entcs.2004.12.021_bib009","series-title":"The Temporal Logic of Reactive and Concurrent Systems: Safety","author":"Manna","year":"1995"},{"key":"10.1016\/j.entcs.2004.12.021_bib010","series-title":"Symbolic Model Checking","author":"McMillan","year":"1993"},{"key":"10.1016\/j.entcs.2004.12.021_bib011","unstructured":"Sajid, K. and R. Kaviola, Verification of pentiumTM4 BUS recycle logic using symbolic simulation and induction, in: Intel Design Test and Technology Conference, 2003"},{"key":"10.1016\/j.entcs.2004.12.021_bib012","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/BF01383966","article-title":"Formal verification by symbolic evaluation of partially-ordered trajectories","volume":"6","author":"Seger","year":"1995","journal-title":"Formal Methods in System Design"},{"key":"10.1016\/j.entcs.2004.12.021_bib013","series-title":"Proc. 3rd Conference on Formal Methods in Computer-Aided Design","first-page":"108","article-title":"Check safety properties using induction and a SAT-solver","volume":"1954","author":"Sheeran","year":"2000"},{"key":"10.1016\/j.entcs.2004.12.021_bib014","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1994.1092","article-title":"Reasoning about infinite computations","volume":"115","author":"Vardi","year":"1994","journal-title":"Information and Computation"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105000873?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105000873?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,1,28]],"date-time":"2019-01-28T07:22:21Z","timestamp":1548660141000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066105000873"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,3]]},"references-count":14,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2005,3]]}},"alternative-id":["S1571066105000873"],"URL":"https:\/\/doi.org\/10.1016\/j.entcs.2004.12.021","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2005,3]]}}}