{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,29]],"date-time":"2026-05-29T11:32:28Z","timestamp":1780054348146,"version":"3.54.0"},"reference-count":14,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1109\/iri.2004.1431509","type":"proceedings-article","created":{"date-parts":[[2005,5,24]],"date-time":"2005-05-24T10:52:03Z","timestamp":1116931923000},"page":"493-498","source":"Crossref","is-referenced-by-count":17,"title":["Specification-based testing with linear temporal logic"],"prefix":"10.1109","author":[{"family":"Li Tan","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"O.","family":"Sokolsky","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"family":"Insup Lee","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"13","article-title":"Property-coverage testing","volume":"ms cis 3 2","author":"tan","year":"2003","journal-title":"Technical Report"},{"key":"14","author":"yang","year":"1998","journal-title":"SMV Models"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1145\/154183.154190"},{"key":"12","article-title":"Evidence-based model checking","author":"tan","year":"2002","journal-title":"CAV '02"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.1995.249985"},{"key":"2","article-title":"Efficient detection of vacuity in ACTL formulas","author":"beer","year":"1997","journal-title":"CAV '97"},{"key":"1","doi-asserted-by":"publisher","DOI":"10.1142\/S0218539301000530"},{"key":"10","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"7","article-title":"A temporal logic based theory of test coverage and generation","author":"hong","year":"2002","journal-title":"TACAS'02"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1016\/0167-739X(86)90022-1"},{"key":"4","article-title":"Expressibility results for linear-time and branching-time logics","volume":"354","author":"clarke","year":"1989","journal-title":"REX Workshop"},{"key":"9","doi-asserted-by":"publisher","DOI":"10.1109\/5.533956"},{"key":"8","article-title":"Vacuity detection in temporal model checking","author":"kupferman","year":"1999","journal-title":"Proc CHARME'99"}],"event":{"name":"2004 IEEE International Conference on Information Reuse and Integration, 2004. IRI 2004.","location":"Las Vegas, NV, USA"},"container-title":["Proceedings of the 2004 IEEE International Conference on Information Reuse and Integration, 2004. IRI 2004."],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/9790\/30875\/01431509.pdf?arnumber=1431509","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,3,15]],"date-time":"2017-03-15T00:23:02Z","timestamp":1489537382000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1431509\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":14,"URL":"https:\/\/doi.org\/10.1109\/iri.2004.1431509","relation":{},"subject":[]}}