{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:15:20Z","timestamp":1750306520971,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":12,"publisher":"ACM","license":[{"start":{"date-parts":[[2014,11,11]],"date-time":"2014-11-11T00:00:00Z","timestamp":1415664000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2014,11,11]]},"DOI":"10.1145\/2635868.2661669","type":"proceedings-article","created":{"date-parts":[[2014,11,4]],"date-time":"2014-11-04T21:44:36Z","timestamp":1415137476000},"page":"731-734","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["Aalta: an LTL satisfiability checker over Infinite\/Finite traces"],"prefix":"10.1145","author":[{"given":"Jianwen","family":"Li","sequence":"first","affiliation":[{"name":"East China Normal University, China"}]},{"given":"Yinbo","family":"Yao","sequence":"additional","affiliation":[{"name":"East China Normal University, China"}]},{"given":"Geguang","family":"Pu","sequence":"additional","affiliation":[{"name":"East China Normal University, China"}]},{"given":"Lijun","family":"Zhang","sequence":"additional","affiliation":[{"name":"Institute of Software at Chinese Academy of Sciences, China"}]},{"given":"Jifeng","family":"He","sequence":"additional","affiliation":[{"name":"East China Normal University, China"}]}],"member":"320","published-online":{"date-parts":[[2014,11,11]]},"reference":[{"key":"e_1_3_2_1_1_1","first-page":"364","volume-title":"Computer Aided Verification","author":"Cimatti A.","unstructured":"A. Cimatti , E.M. Clarke , E. Giunchiglia , F. Giunchiglia , M. Pistore , M. Roveri , R. Sebastiani , and A. Tacchella . Nusmv 2: An opensource tool for symbolic model checking . In Computer Aided Verification , pages 359\u2013 364 . Springer, 2002. A. Cimatti, E.M. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella. Nusmv 2: An opensource tool for symbolic model checking. In Computer Aided Verification, pages 359\u2013364. Springer, 2002."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/647868.737111"},{"key":"e_1_3_2_1_3_1","first-page":"2007","volume-title":"Proceedings of the 24th International Joint Conference on Artificial Intelligence, IJCAI\u201913","author":"De Giacomo G.","unstructured":"G. De Giacomo and M. Y. Vardi . Linear temporal logic and linear dynamic logic on finite traces . In Proceedings of the 24th International Joint Conference on Artificial Intelligence, IJCAI\u201913 , pages 2000\u2013 2007 . AAAI Press, 2013. G. De Giacomo and M. Y. Vardi. Linear temporal logic and linear dynamic logic on finite traces. In Proceedings of the 24th International Joint Conference on Artificial Intelligence, IJCAI\u201913, pages 2000\u20132007. AAAI Press, 2013."},{"key":"e_1_3_2_1_4_1","volume-title":"Polsat: A portfolio ltl satisfiability solver. CoRR, abs\/1311.1602","author":"Li J.","year":"2013","unstructured":"J. Li , G. Pu , L. Zhang , M. Y. Vardi , and J. He . Polsat: A portfolio ltl satisfiability solver. CoRR, abs\/1311.1602 , 2013 . J. Li, G. Pu, L. Zhang, M. Y. Vardi, and J. He. Polsat: A portfolio ltl satisfiability solver. CoRR, abs\/1311.1602, 2013."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIME.2013.19"},{"key":"e_1_3_2_1_6_1","volume-title":"Fast LTL Satisfiability Checking by SAT Solvers. CoRR, abs\/1401.5677","author":"Li J.","year":"2014","unstructured":"J. Li , G. Pu , L. Zhang , M. Y. Vardi , and J. He . Fast LTL Satisfiability Checking by SAT Solvers. CoRR, abs\/1401.5677 , 2014 . J. Li, G. Pu, L. Zhang, M. Y. Vardi, and J. He. Fast LTL Satisfiability Checking by SAT Solvers. CoRR, abs\/1401.5677, 2014."},{"key":"e_1_3_2_1_7_1","first-page":"96","volume-title":"The 21th European Conference on Artificial Intelligence","author":"Li J.","year":"2014","unstructured":"J. Li , L. Zhang , G. Pu , M. Y. Vardi , and J. He . LT L f satisfibility checking . In The 21th European Conference on Artificial Intelligence , pages 91\u2013 96 , 2014 . J. Li, L. Zhang, G. Pu, M. Y. Vardi, and J. He. LT L f satisfibility checking. In The 21th European Conference on Artificial Intelligence, pages 91\u201396, 2014."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-010-0140-3"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11623-0_7"},{"key":"e_1_3_2_1_11_1","first-page":"292","volume-title":"Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods","author":"Schwendimann S.","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 , pages 277\u2013 292 . Springer-Verlag, 1998. 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, pages 277\u2013292. Springer-Verlag, 1998."},{"key":"e_1_3_2_1_12_1","volume-title":"Springer","author":"Vardi M. Y.","year":"1996","unstructured":"M. Y. Vardi . An automata-theoretic approach to linear temporal logic. In Logics for Concurrency: Structure versus Automata, pages 238\u2013266 . Springer , 1996 . M. Y. Vardi. An automata-theoretic approach to linear temporal logic. In Logics for Concurrency: Structure versus Automata, pages 238\u2013266. Springer, 1996."}],"event":{"name":"SIGSOFT\/FSE'14: 22nd ACM SIGSOFT Symposium on the Foundations of Software Engineering","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"],"location":"Hong Kong China","acronym":"SIGSOFT\/FSE'14"},"container-title":["Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2635868.2661669","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2635868.2661669","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:11:57Z","timestamp":1750227117000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2635868.2661669"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,11,11]]},"references-count":12,"alternative-id":["10.1145\/2635868.2661669","10.1145\/2635868"],"URL":"https:\/\/doi.org\/10.1145\/2635868.2661669","relation":{},"subject":[],"published":{"date-parts":[[2014,11,11]]},"assertion":[{"value":"2014-11-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}