{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,28]],"date-time":"2025-11-28T17:20:15Z","timestamp":1764350415328},"reference-count":27,"publisher":"Oxford University Press (OUP)","issue":"6","license":[{"start":{"date-parts":[[2018,4,12]],"date-time":"2018-04-12T00:00:00Z","timestamp":1523491200000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/academic.oup.com\/journals\/pages\/about_us\/legal\/notices"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018,9,5]]},"DOI":"10.1093\/logcom\/exy013","type":"journal-article","created":{"date-parts":[[2018,3,20]],"date-time":"2018-03-20T20:24:43Z","timestamp":1521577483000},"page":"1011-1030","source":"Crossref","is-referenced-by-count":6,"title":["Accelerating LTL satisfiability checking by SAT solvers"],"prefix":"10.1093","volume":"28","author":[{"given":"Jianwen","family":"Li","sequence":"first","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Geguang","family":"Pu","sequence":"additional","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lijun","family":"Zhang","sequence":"additional","affiliation":[{"name":"State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Moshe Y","family":"Vardi","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Rice University, Houston, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jifeng","family":"He","sequence":"additional","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"286","published-online":{"date-parts":[[2018,4,12]]},"reference":[{"key":"key\n\t\t\t\t20180903132124_C1","doi-asserted-by":"crossref","unstructured":"N. Amla , X.Du and A.Kuehlmann. An analysis of sat-based model checking techniques in an industrial environment. In 13th IFIG Advanced Research Working Conference on Correct Hardware Design and Verification Methods, D.Borrione and W.Paul, eds, pp. 254\u2013268. Saarbr\u00fccken, Germany, 2005.","DOI":"10.1007\/11560548_20"},{"key":"key\n\t\t\t\t20180903132124_C2","doi-asserted-by":"crossref","first-page":"160","DOI":"10.1016\/S1571-0661(04)80410-9","article-title":"Liveness checking as safety checking","volume":"66","author":"Biere","year":"2002","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"key\n\t\t\t\t20180903132124_C3","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","article-title":"Sat-based model checking without unrolling","author":"Bradley","year":"2011","journal-title":"Verification, Model Checking, and Abstract Interpretation"},{"key":"key\n\t\t\t\t20180903132124_C4","unstructured":"A. Bradley , F.Somenzi and Z.Hassan. An incremental approach to model checking progress properties. In Proceedings of the International Conference on Formal Methods in Computer-Aided Design, pp. 144\u2013153. FMCAD Inc.: Austin, USA, 2011."},{"key":"key\n\t\t\t\t20180903132124_C5","doi-asserted-by":"crossref","unstructured":"A. Cimatti , E. M.Clarke, E.Giunchiglia and F.Giunchiglia. Nusmv 2: an opensource tool for symbolic model checking. In International Conference on Computer Aided Verification, E. B. Guldstrand and K. Larsen, eds.pp. 359\u2013364. Copenhagen, Denmark, 2002.","DOI":"10.1007\/3-540-45657-0_29"},{"key":"key\n\t\t\t\t20180903132124_C6","doi-asserted-by":"crossref","first-page":"174","DOI":"10.1007\/s10009-004-0182-5","article-title":"Computational challenges in bounded model checking","volume":"7","author":"Clarke","year":"2005","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"key\n\t\t\t\t20180903132124_C7","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1011276507260","article-title":"Bounded model checking using satisfiability solving","volume":"19","author":"Clarke","year":"2001","journal-title":"Formal Methods in System Design"},{"key":"key\n\t\t\t\t20180903132124_C8","doi-asserted-by":"crossref","unstructured":"M. De Wulf , L.Doyen and N.Maquet. Antichains: alternative algorithms for ltl satisfiability and model-checking. In Tools and Algorithms for the Construction and Analysis of Systems, C. R. Ramakrishnan and J. Rehof, eds, pp. 63\u201377. Budapest, Hungary, 2008.","DOI":"10.1007\/978-3-540-78800-3_6"},{"key":"key\n\t\t\t\t20180903132124_C9","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1007\/s00236-007-0062-z","article-title":"A decision procedure for propositional projection temporal logic with infinite models","volume":"45","author":"Duan","year":"2008","journal-title":"Acta Informatica"},{"key":"key\n\t\t\t\t20180903132124_C10","first-page":"7","article-title":"Property specification patterns for finite-state verification","author":"Dwyer","year":"1998","journal-title":"Proceedings of the Second Workshop on Formal Methods in Software Practice"},{"key":"key\n\t\t\t\t20180903132124_C11","doi-asserted-by":"crossref","unstructured":"N. E\u00e9n and N. S\u00f6rensson. An extensible sat-solver. In International Conference on Theory and Applications of Satisfiability Testing, E. Giunchiglia and A. Tacchella, eds, pp. 502\u2013518. Santa Margherita Ligure, Italy, 2003.","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"key\n\t\t\t\t20180903132124_C12","doi-asserted-by":"crossref","first-page":"429","DOI":"10.1093\/logcom\/7.4.429","article-title":"A normal form for temporal logics and its applications in theorem-proving and execution","volume":"7","author":"Fisher","year":"1997","journal-title":"Journal of Logic and Computation"},{"key":"key\n\t\t\t\t20180903132124_C13","doi-asserted-by":"crossref","unstructured":"R. Gerth , D.Peled and M. Y.Vardi. Simple on-the-fly automatic verification of linear temporal logic. In Protocol Specification, Testing, and Verification, P.Dembiski and M.Sredniawa, eds, pp. 3\u201318. Warsaw, Poland, 1995.","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"key\n\t\t\t\t20180903132124_C14","first-page":"274","article-title":"Trp++ 2.0: a temporal resolution prover","author":"Hustadt","year":"2003","journal-title":"International Conference on Automated Deduction"},{"key":"key\n\t\t\t\t20180903132124_C15","article-title":"Polsat: a portfolio ltl satisfiability solver","author":"Li","year":"2013"},{"key":"key\n\t\t\t\t20180903132124_C16","doi-asserted-by":"crossref","unstructured":"J. Li , L.Zhang, and G.Pu. LTL satisfibility checking revisited. In The 20th International Symposium on Temporal Representation and Reasoning, C. Sanchez, K. B. Venable and E. Zimanyi, eds, pp. 91\u201398. Pensacola, Florida, USA, 2013.","DOI":"10.1109\/TIME.2013.19"},{"key":"key\n\t\t\t\t20180903132124_C17","doi-asserted-by":"crossref","first-page":"76","DOI":"10.1145\/1536616.1536637","article-title":"Boolean satisfiability from theoretical hardness to practical success","volume":"52","author":"Malik","year":"2009","journal-title":"Communication of ACM"},{"key":"key\n\t\t\t\t20180903132124_C18","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","article-title":"Interpolation and SAT-based model checking","volume-title":"International Conference on Computer Aided Verification","author":"McMillan","year":"2003"},{"key":"key\n\t\t\t\t20180903132124_C19","doi-asserted-by":"crossref","unstructured":"M. M. Pourhashem Kallehbasti . Scalable formal verification of UML models. In EEE\/ACM 37th IEEE International Conference on Software Engineering, pp. 847\u2013850. Piscataway, NJ, USA, 2015.","DOI":"10.1109\/ICSE.2015.275"},{"key":"key\n\t\t\t\t20180903132124_C22","doi-asserted-by":"crossref","unstructured":"K. Y. Rozier . Specification: The Biggest Bottleneck in Formal Methods and Autonomy. In 8th International Conference on Verified Software. Theories, Tools, and Experiments, S. Blazy and M. Chechik, eds, pp. 8\u201326. Toronto, Canada, 2016.","DOI":"10.1007\/978-3-319-48869-1_2"},{"key":"key\n\t\t\t\t20180903132124_C20","doi-asserted-by":"crossref","first-page":"1230","DOI":"10.1007\/s10009-010-0140-3","article-title":"LTL satisfiability checking","volume":"12","author":"Rozier","year":"2010","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"key\n\t\t\t\t20180903132124_C21","doi-asserted-by":"crossref","unstructured":"K. Y. Rozier and M. Y.Vardi. A multi-encoding approach for LTL symbolic satisfiability checking. In Proceedings of the 17th International Conference on Formal Methods, M. Hinchey, ed., pp. 417\u2013431. Limerick, Ireland, 2011.","DOI":"10.1007\/978-3-642-21437-0_31"},{"key":"key\n\t\t\t\t20180903132124_C23","doi-asserted-by":"crossref","unstructured":"V. Schuppan and L.Darmawan. Evaluating LTL satisfiability solvers. In Proceedings of the 9th International Conference on Automated Technology for Verification and Analysis, T. Bultan and P. Hsiung, eds, pp. 397\u2013413. Taipei, Taiwan, 2011.","DOI":"10.1007\/978-3-642-24372-1_28"},{"key":"key\n\t\t\t\t20180903132124_C24","doi-asserted-by":"crossref","unstructured":"S. Schwendimann . A new one-pass tableau calculus for pltl. In Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, H. D.Swart ed., pp. 277\u2013292. Oisterwijk, Netherlands, 1998.","DOI":"10.1007\/3-540-69778-0_28"},{"key":"key\n\t\t\t\t20180903132124_C25","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","article-title":"The complexity of propositional linear temporal logic","volume":"32","author":"Sistla","year":"1985","journal-title":"Journal of the ACM"},{"key":"key\n\t\t\t\t20180903132124_C26","doi-asserted-by":"crossref","first-page":"537","DOI":"10.1007\/978-3-642-31365-3_42","article-title":"A pltl-prover based on labelled superposition with partial model guidance","author":"Suda","year":"2012","journal-title":"International Joint Conference on Automated Reasoning"},{"key":"key\n\t\t\t\t20180903132124_C27","doi-asserted-by":"crossref","first-page":"391","DOI":"10.1007\/978-3-642-28717-6_31","article-title":"Labelled Superposition for PLTL","author":"Suda","year":"2012","journal-title":"International Conference on Logic for Programming, Artificial Intelligence, and Reasoning"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/28\/6\/1011\/25677703\/exy013.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,16]],"date-time":"2022-08-16T15:27:25Z","timestamp":1660663645000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/28\/6\/1011\/4964975"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,4,12]]},"references-count":27,"journal-issue":{"issue":"6","published-online":{"date-parts":[[2018,4,12]]},"published-print":{"date-parts":[[2018,9,5]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exy013","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"value":"0955-792X","type":"print"},{"value":"1465-363X","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2018,9]]},"published":{"date-parts":[[2018,4,12]]}}}