{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T20:15:03Z","timestamp":1761941703130,"version":"build-2065373602"},"reference-count":27,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1109\/iccad.2005.1560185","type":"proceedings-article","created":{"date-parts":[[2005,12,22]],"date-time":"2005-12-22T17:52:37Z","timestamp":1135273957000},"page":"877-884","source":"Crossref","is-referenced-by-count":14,"title":["Efficient LTL compilation for SAT-based model checking"],"prefix":"10.1109","author":[{"given":"R.","family":"Armoni","sequence":"first","affiliation":[]},{"given":"S.","family":"Egorov","sequence":"additional","affiliation":[]},{"given":"R.","family":"Fraer","sequence":"additional","affiliation":[]},{"given":"D.","family":"Korchemny","sequence":"additional","affiliation":[]},{"given":"M.Y.","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"19","doi-asserted-by":"crossref","first-page":"538","DOI":"10.1007\/10722167_40","article-title":"FoCs - Automatic generation of simulation checkers from formal specifications","author":"abarbanel","year":"2000","journal-title":"Proc Computer Aided Verification"},{"key":"17","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011254632723"},{"key":"18","first-page":"319","article-title":"On the complexity of co-automata","author":"safra","year":"1988","journal-title":"Proc 35th Symp Foundations of Computer Science"},{"key":"15","doi-asserted-by":"crossref","first-page":"350","DOI":"10.1007\/11513988_35","article-title":"Symbolic systems, explicit properties: On hybrid approaches for LTL symbolic model checking","author":"sebastiani","year":"2005","journal-title":"Proc Computer Aided Verification"},{"key":"16","doi-asserted-by":"publisher","DOI":"10.1007\/BF01782772"},{"key":"13","doi-asserted-by":"crossref","DOI":"10.1007\/s10009-004-0182-5","article-title":"Computational challenges in bounded model checking","author":"clarke","year":"2005","journal-title":"Int J Softw Tools for Technol Transfer"},{"key":"14","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1007\/978-3-540-27813-9_18","article-title":"GSTE is partitioned model checking","author":"sebastiani","year":"2004","journal-title":"Proc Computer Aided Verification"},{"key":"11","doi-asserted-by":"crossref","first-page":"126","DOI":"10.1007\/978-3-540-39724-3_12","article-title":"More deterministic vs. \"Smaller\" bu?chi automata for efficient LTL model checking","author":"sebastiani","year":"2003","journal-title":"Proc Correct Hardware Designs and Verification Methods CHARME 95"},{"key":"12","first-page":"415","article-title":"Another look at LTL model checking","author":"clarke","year":"1994","journal-title":"Proc Computer Aided Verification"},{"key":"21","first-page":"108","article-title":"Checking safety properties using induction and a SAT-solver","author":"sheeran","year":"2000","journal-title":"Proc Formal Methods in Computer-Aided Design"},{"key":"20","doi-asserted-by":"publisher","DOI":"10.1109\/TEST.2002.1041761"},{"key":"22","doi-asserted-by":"publisher","DOI":"10.1145\/322234.322243"},{"journal-title":"Introduction to Automata Theory Languages and Computation","year":"1979","author":"hopcroft","key":"23"},{"key":"24","first-page":"157","article-title":"State space reductions for alternating Bu?chi automata: Quotienting by simulation equivalences","author":"fritz","year":"2002","journal-title":"Proc of FSTTCS"},{"key":"25","first-page":"157","article-title":"An automata-theoretic approach to linear temporal logic","author":"vardi","year":"2002","journal-title":"Logic for Concurrency Structure Vs Automata"},{"key":"26","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.12.021"},{"key":"27","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.07.019"},{"journal-title":"Model checking","year":"1999","author":"clarke","key":"3"},{"journal-title":"Property Specification Language Reference Manual Version 1 1","year":"2004","key":"2"},{"key":"1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"10","doi-asserted-by":"crossref","first-page":"248","DOI":"10.1007\/10722167_21","article-title":"Efficient Bu?chi automata from LTL formulae","author":"somenzi","year":"2000","journal-title":"Proc Computer Aided Verification"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.1999.781333"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1007\/BF00121128"},{"key":"4","first-page":"332","article-title":"An automata-theoretic approach to automatic program verification","author":"vardi","year":"1986","journal-title":"Proc Symp Logic Comput Sci"},{"key":"9","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1007\/3-540-48683-6_23","article-title":"Improved automata generation for linear temporal logic","author":"daniele","year":"1999","journal-title":"Proc Computer Aided Verification"},{"key":"8","first-page":"3","article-title":"Simple on-the-fly automatic verification of linear temporal logic","author":"gerth","year":"1995","journal-title":"Protocol Specification Testing and Verification IX"}],"event":{"name":"ICCAD-2005. IEEE\/ACM International Conference on Computer-Aided Design, 2005.","location":"San Jose, CA"},"container-title":["ICCAD-2005. IEEE\/ACM International Conference on Computer-Aided Design, 2005."],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/10431\/33130\/01560185.pdf?arnumber=1560185","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,17]],"date-time":"2017-06-17T01:55:34Z","timestamp":1497664534000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1560185\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":27,"URL":"https:\/\/doi.org\/10.1109\/iccad.2005.1560185","relation":{},"subject":[]}}