{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T16:39:18Z","timestamp":1776530358286,"version":"3.51.2"},"reference-count":37,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"11","license":[{"start":{"date-parts":[[2008,11,1]],"date-time":"2008-11-01T00:00:00Z","timestamp":1225497600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst."],"published-print":{"date-parts":[[2008,11]]},"DOI":"10.1109\/tcad.2008.2006092","type":"journal-article","created":{"date-parts":[[2008,10,22]],"date-time":"2008-10-22T14:53:47Z","timestamp":1224687227000},"page":"2068-2082","source":"Crossref","is-referenced-by-count":51,"title":["Unbounded Protocol Compliance Verification Using Interval Property Checking With Invariants"],"prefix":"10.1109","volume":"27","author":[{"given":"Minh D.","family":"Nguyen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Max","family":"Thalmaier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Markus","family":"Wedler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J\u00d6rg","family":"Bormann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dominik","family":"Stoffel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wolfgang","family":"Kunz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"1","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.1990.114827"},{"key":"2","first-page":"193","article-title":"Symbolic model checking without BDDs","author":"Biere","year":"1999","journal-title":"Proc. Int. Conf. TACAS"},{"key":"3"},{"key":"4","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.1996.563525"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.1997.597241"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1109\/EURDAC.1996.558201"},{"key":"7","first-page":"126","article-title":"A unified framework for the formal verification of sequential circuits","author":"Coudert","year":"1990","journal-title":"Proc. ICCAD"},{"key":"8","first-page":"23","author":"Moon","year":"2000","journal-title":"Proc. Int. DAC"},{"key":"9","doi-asserted-by":"publisher","DOI":"10.1109\/43.552080"},{"key":"10","doi-asserted-by":"publisher","DOI":"10.1109\/43.552079"},{"key":"11","first-page":"451","article-title":"Approximate reachability with BDDs using overlapping projections","author":"Govindaraju","year":"1998","journal-title":"Proc. Int. DAC"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.1999.810618"},{"key":"13","doi-asserted-by":"publisher","DOI":"10.1109\/TVLSI.2003.812320"},{"key":"14","first-page":"229","article-title":"GSTE is partitioned model checking","author":"Sebastiani","year":"2004","journal-title":"Proc. Int. Conf. CAV"},{"key":"15","first-page":"170","article-title":"Reasoning about GSTE assertion graphs","volume":"2860, Lecture","author":"Hu","year":"2003","journal-title":"Proc. 12th IFIP WG 10.5 Adv. Res. Working Conf. (CHARME)"},{"key":"16","first-page":"154","article-title":"Counterexample-guided abstraction refinement","author":"Clarke","year":"2000","journal-title":"Proc. Int. Conf. CAV"},{"key":"17","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2006.873897"},{"key":"18","first-page":"33","article-title":"Automated abstraction refinement for model checking large state spaces using SAT based conflict analysis","author":"Chauhan","year":"2002","journal-title":"Proc. Int. Conf. FMCAD"},{"key":"19","first-page":"2","article-title":"Automatic abstraction without counterexamples","author":"McMillan","year":"2003","journal-title":"Proc. Int. Conf. TACAS"},{"key":"20","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2003.1257811"},{"key":"21","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2007.907270"},{"key":"22","first-page":"108","article-title":"Checking safety properties using induction and a SAT-solver","author":"Sheeran","year":"2000","journal-title":"Proc. Int. Conf. FMCAD"},{"key":"23","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2004.1268843"},{"key":"24","author":"","year":"2005","journal-title":"Verfahren zur Bestimmung der G\u00dcte einer Menge von Eigenschaften (Method for determining the quality of a set of properties)"},{"key":"25","volume":"58","author":"Biere","year":"2003","journal-title":"Advances in Computers"},{"key":"26","doi-asserted-by":"publisher","DOI":"10.1109\/43.275352"},{"key":"27","journal-title":"Debussy nWave"},{"key":"28","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2005.1560219"},{"key":"29","first-page":"250","article-title":"Applying SAT methods in unbounded symbolic model checking","author":"McMillan","year":"2002","journal-title":"Proc. Int. Conf. CAV"},{"key":"30","first-page":"502","article-title":"An extensible SAT-solver","author":"Een","year":"2003","journal-title":"Proc. Int. Conf. Theory Appl. SAT"},{"key":"31","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2004.1382631"},{"key":"32","author":"Somenzi","journal-title":"CUDD: CU Decision Diagram Package"},{"key":"33","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.1997.597145"},{"key":"34","first-page":"428","article-title":"VIS: A system for verification and synthesis","volume":"1102","author":"Brayton","year":"1996","journal-title":"Proc. Int. Conf. CAV"},{"key":"35","author":"Nguyen","journal-title":"Public Benchmarks for Evaluation of the TBT Algorithm"},{"key":"36","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2000.840831"},{"key":"37","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.1995.480006"}],"container-title":["IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/43\/4655545\/04655556.pdf?arnumber=4655556","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,29]],"date-time":"2021-11-29T15:40:14Z","timestamp":1638200414000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/4655556\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,11]]},"references-count":37,"journal-issue":{"issue":"11"},"URL":"https:\/\/doi.org\/10.1109\/tcad.2008.2006092","relation":{},"ISSN":["0278-0070"],"issn-type":[{"value":"0278-0070","type":"print"}],"subject":[],"published":{"date-parts":[[2008,11]]}}}