{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,15]],"date-time":"2025-11-15T10:36:13Z","timestamp":1763202973600,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":67,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"National Natural Science Foundation of China","award":["62276284, 61976232, 61876204, 51978675"],"award-info":[{"award-number":["62276284, 61976232, 61876204, 51978675"]}]},{"name":"Guangdong Basic and Applied Basic Research Foundation","award":["2023A1515011470, 2022A1515011355"],"award-info":[{"award-number":["2023A1515011470, 2022A1515011355"]}]},{"name":"Guangzhou Science and Technology Project","award":["202201011699"],"award-info":[{"award-number":["202201011699"]}]},{"name":"Shenzhen Science and Technology Program","award":["KJZD2023092311405902"],"award-info":[{"award-number":["KJZD2023092311405902"]}]},{"name":"Guizhou Provincial Science and Technology Projects","award":["2022-259"],"award-info":[{"award-number":["2022-259"]}]},{"name":"Humanities and Social Science Research Project of Ministry of Education","award":["18YJCZH006"],"award-info":[{"award-number":["18YJCZH006"]}]},{"name":"the Fundamental Research Funds for the Central Universities, Sun Yat-sen University","award":["23ptpy31"],"award-info":[{"award-number":["23ptpy31"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,9,11]]},"DOI":"10.1145\/3650212.3680337","type":"proceedings-article","created":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T11:44:25Z","timestamp":1726055065000},"page":"996-1008","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Learning to Check LTL Satisfiability and to Generate Traces via Differentiable Trace Checking"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3733-9361","authenticated-orcid":false,"given":"Weilin","family":"Luo","sequence":"first","affiliation":[{"name":"Sun Yat-sen University, Guangzhou, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4866-4159","authenticated-orcid":false,"given":"Pingjia","family":"Liang","sequence":"additional","affiliation":[{"name":"Sun Yat-sen University, Guangzhou, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8315-9337","authenticated-orcid":false,"given":"Junming","family":"Qiu","sequence":"additional","affiliation":[{"name":"Sun Yat-sen University, Guangzhou, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-6025-0567","authenticated-orcid":false,"given":"Polong","family":"Chen","sequence":"additional","affiliation":[{"name":"Sun Yat-sen University, Guangzhou, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5357-9130","authenticated-orcid":false,"given":"Hai","family":"Wan","sequence":"additional","affiliation":[{"name":"Sun Yat-sen University, Guangzhou, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7541-1387","authenticated-orcid":false,"given":"Jianfeng","family":"Du","sequence":"additional","affiliation":[{"name":"Guangdong University of Foreign Studies, Guangzhou, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-6149-297X","authenticated-orcid":false,"given":"Weiyuan","family":"Fang","sequence":"additional","affiliation":[{"name":"Sun Yat-sen University, Guangzhou, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,9,11]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Saeed Amizadeh Sergiy Matusevych and Markus Weimer. 2019. Learning To Solve Circuit-SAT: An Unsupervised Differentiable Approach. In ICLR."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1108\/17563780911005818"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","unstructured":"Irwan Bello Hieu Pham Quoc V. Le Mohammad Norouzi and Samy Bengio. 2017. Neural Combinatorial Optimization with Reinforcement Learning. In ICLR. https:\/\/doi.org\/10.48550\/arXiv.1611.09940 10.48550\/arXiv.1611.09940","DOI":"10.48550\/arXiv.1611.09940"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3092703.3098239"},{"key":"e_1_3_2_1_5_1","volume-title":"Leviathan: A New LTL Satisfiability Checking Tool Based on a One-Pass Tree-Shaped Tableau. In IJCAI. 950\u2013956.","author":"Bertello Matteo","year":"2016","unstructured":"Matteo Bertello, Nicola Gigante, Angelo Montanari, and Mark Reynolds. 2016. Leviathan: A New LTL Satisfiability Checking Tool Based on a One-Pass Tree-Shaped Tableau. In IJCAI. 950\u2013956."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49059-0_14"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.09.004"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_36"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","unstructured":"Roberto Cavada Alessandro Cimatti Michele Dorigatti Alberto Griggio Alessandro Mariotti Andrea Micheli Sergio Mover Marco Roveri and Stefano Tonetta. 2014. The nuXmv symbolic model checker. In CAV. 334\u2013342. https:\/\/doi.org\/10.1007\/978-3-319-08867-9_22 10.1007\/978-3-319-08867-9_22","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.is.2015.06.009"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-47813-2_14"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011276507260"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","unstructured":"Matthias Cosler Frederik Schmitt Christopher Hahn and Bernd Finkbeiner. 2023. Iterative Circuit Repair Against Formal Specifications. In ICLR. https:\/\/doi.org\/10.48550\/arXiv.2303.01158 10.48550\/arXiv.2303.01158","DOI":"10.48550\/arXiv.2303.01158"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","unstructured":"Renzo Degiovanni Facundo Molina Germ\u00e1n Regis and Nazareno Aguirre. 2018. A genetic algorithm for goal-conflict identification. In ASE. 520\u2013531. https:\/\/doi.org\/10.1145\/3238147.3238220 10.1145\/3238147.3238220","DOI":"10.1145\/3238147.3238220"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"crossref","unstructured":"Alexandre Duret-Lutz Alexandre Lewkowicz Amaury Fauchille Thibaud Michaud Etienne Renault and Laurent Xu. 2016. Spot 2.0 - A Framework for LTL and \u03c9 -Automata Manipulation. In ATVA. 122\u2013129.","DOI":"10.1007\/978-3-319-46520-3_8"},{"key":"e_1_3_2_1_17_1","volume-title":"Brayton","author":"E\u00e9n Niklas","year":"2011","unstructured":"Niklas E\u00e9n, Alan Mishchenko, and Robert K. Brayton. 2011. Efficient implementation of property directed reachability. In FMCAD. 125\u2013134."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1613\/jair.1.11256"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/371282.371311"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_1"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2003.04218"},{"key":"e_1_3_2_1_22_1","unstructured":"William L. Hamilton Zhitao Ying and Jure Leskovec. 2017. Inductive Representation Learning on Large Graphs. In NeurIPS. 1024\u20131034."},{"key":"e_1_3_2_1_23_1","unstructured":"Nikolaos Karalias and Andreas Loukas. 2020. Erdos Goes Neural: an Unsupervised Learning Framework for Combinatorial Optimization on Graphs. In NeurIPS."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56922-7_9"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","unstructured":"Guillaume Lample and Fran\u00e7ois Charton. 2020. Deep Learning For Symbolic Mathematics. In ICLR. https:\/\/doi.org\/10.48550\/arXiv.1912.01412 10.48550\/arXiv.1912.01412","DOI":"10.48550\/arXiv.1912.01412"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","unstructured":"Jianwen Li Yinbo Yao Geguang Pu Lijun Zhang and Jifeng He. 2014. Aalta: an LTL satisfiability checker over Infinite\/Finite traces. In FSE. 731\u2013734. https:\/\/doi.org\/10.1145\/2635868.2661669 10.1145\/2635868.2661669","DOI":"10.1145\/2635868.2661669"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","unstructured":"Jianwen Li Lijun Zhang Geguang Pu Moshe Y. Vardi and Jifeng He. 2013. LTL Satisfiability Checking Revisited. In TIME. 91\u201398. https:\/\/doi.org\/10.1109\/TIME.2013.19 10.1109\/TIME.2013.19","DOI":"10.1109\/TIME.2013.19"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-26287-1_13"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-018-00326-5"},{"key":"e_1_3_2_1_31_1","unstructured":"Zhaoyu Li and Xujie Si. 2022. NSNet: A General Neural Probabilistic Framework for Satisfiability Problems. In NeurIPS."},{"key":"e_1_3_2_1_32_1","unstructured":"ARM Ltd.. 1999. AMBA Specification (Rev. 2)."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","unstructured":"Weilin Luo Pingjia Liang Jianfeng Du Hai Wan Bo Peng and Delong Zhang. 2022. Bridging LTLf Inference to GNN Inference for Learning LTLf Formulae. In AAAI. 9849\u20139857. https:\/\/doi.org\/10.1609\/aaai.v36i9.21221 10.1609\/aaai.v36i9.21221","DOI":"10.1609\/aaai.v36i9.21221"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"crossref","unstructured":"Weilin Luo Hai Wan Jianfeng Du Xiaoda Li Yuze Fu Rongzhen Ye and Delong Zhang. 2022. Teaching LTLf Satisfiability Checking to Neural Networks. In IJCAI. 3292\u20133298.","DOI":"10.24963\/ijcai.2022\/457"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","unstructured":"Weilin Luo Hai Wan Xiaotong Song Binhao Yang Hongzhen Zhong and Yin Chen. 2021. How to Identify Boundary Conditions with Contrasty Metric? In ICSE. 1473\u20131484. https:\/\/doi.org\/10.1109\/ICSE43902.2021.00132 10.1109\/ICSE43902.2021.00132","DOI":"10.1109\/ICSE43902.2021.00132"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3551349.3561163"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE56229.2023.00173"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40176-3_8"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45187-7_17"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2207.11649"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"crossref","unstructured":"Amir Pnueli. 1977. The Temporal Logic of Programs. In FOCS. 46\u201357.","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","unstructured":"Markus Norman Rabe Dennis Lee Kshitij Bansal and Christian Szegedy. 2021. Mathematical Reasoning via Self-supervised Skip-tree Training. In ICLR. https:\/\/doi.org\/10.48550\/arXiv.2006.04757 10.48550\/arXiv.2006.04757","DOI":"10.48550\/arXiv.2006.04757"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73370-6_11"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-010-0140-3"},{"key":"e_1_3_2_1_46_1","unstructured":"Frederik Schmitt Christopher Hahn Markus N. Rabe and Bernd Finkbeiner. 2021. Neural Circuit Synthesis from Specification Patterns. In NeurIPS. 15408\u201315420."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11623-0_7"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2016.01.014"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-015-0242-1"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24372-1_28"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-69778-0_28"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-24258-9_24"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.1802.03685"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3828.3837"},{"key":"e_1_3_2_1_55_1","volume-title":"Ng","author":"Socher Richard","year":"2012","unstructured":"Richard Socher, Brody Huval, Christopher D. Manning, and Andrew Y. Ng. 2012. Semantic Compositionality through Recursive Matrix-Vector Spaces. In EMNLP-CoNLL. 1201\u20131211."},{"key":"e_1_3_2_1_56_1","unstructured":"Richard Socher Alex Perelygin Jean Wu Jason Chuang Christopher D. Manning Andrew Y. Ng and Christopher Potts. 2013. Recursive Deep Models for Semantic Compositionality Over a Sentiment Treebank. In EMNLP. 1631\u20131642."},{"key":"e_1_3_2_1_57_1","first-page":"10497","article-title":"LTL2Action","volume":"139","author":"Vaezipoor Pashootan","year":"2021","unstructured":"Pashootan Vaezipoor, Andrew C. Li, Rodrigo Toro Icarte, and Sheila A. McIlraith. 2021. LTL2Action: Generalizing LTL Instructions for Multi-Task RL. In ICML. 139, 10497\u201310508.","journal-title":"Generalizing LTL Instructions for Multi-Task RL. In ICML."},{"key":"e_1_3_2_1_58_1","unstructured":"Ashish Vaswani Noam Shazeer Niki Parmar Jakob Uszkoreit Llion Jones Aidan N. Gomez Lukasz Kaiser and Illia Polosukhin. 2017. Attention is All you Need. In NeurIPS. 5998\u20136008."},{"key":"e_1_3_2_1_59_1","unstructured":"Haoyu Wang Nan Wu Hang Yang Cong Hao and Pan Li. 2022. Unsupervised Learning for Combinatorial Optimization with Principled Objective Relaxation. In NeurIPS."},{"key":"e_1_3_2_1_60_1","first-page":"6545","article-title":"SATNet: Bridging deep learning and logical reasoning using a differentiable satisfiability solver","volume":"97","author":"Wang Po-Wei","year":"2019","unstructured":"Po-Wei Wang, Priya L. Donti, Bryan Wilder, and J. Zico Kolter. 2019. SATNet: Bridging deep learning and logical reasoning using a differentiable satisfiability solver. In ICML. 97, 6545\u20136554.","journal-title":"ICML."},{"key":"e_1_3_2_1_61_1","unstructured":"Pierre Wolper. 1985. The tableau method for temporal logic: An overview. Logique et Analyse 119\u2013136."},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_6"},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_6"},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"publisher","unstructured":"Yaqi Xie Fan Zhou and Harold Soh. 2021. Embedding Symbolic Temporal Knowledge into Deep Sequential Models. In ICRA. 4267\u20134273. https:\/\/doi.org\/10.1109\/ICRA48506.2021.9561952 10.1109\/ICRA48506.2021.9561952","DOI":"10.1109\/ICRA48506.2021.9561952"},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"publisher","unstructured":"Runxin Xu Fuli Luo Zhiyuan Zhang Chuanqi Tan Baobao Chang Songfang Huang and Fei Huang. 2021. Raise a Child in Large Language Model: Towards Effective and Generalizable Fine-tuning. In EMNLP. 9514\u20139528. https:\/\/doi.org\/10.48550\/arXiv.2109.05687 10.48550\/arXiv.2109.05687","DOI":"10.48550\/arXiv.2109.05687"},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"publisher","unstructured":"Rongzhen Ye Tianqu Zhuang Hai Wan Jianfeng Du Weilin Luo and Pingjia Liang. 2023. A Noise-Tolerant Differentiable Learning Approach for Single Occurrence Regular Expression with Interleaving. In AAAI. 4809\u20134817. https:\/\/doi.org\/10.1609\/aaai.v37i4.25606 10.1609\/aaai.v37i4.25606","DOI":"10.1609\/aaai.v37i4.25606"},{"key":"e_1_3_2_1_67_1","doi-asserted-by":"publisher","unstructured":"Wenjie Zhang Zeyu Sun Qihao Zhu Ge Li Shaowei Cai Yingfei Xiong and Lu Zhang. 2020. NLocalSAT: Boosting Local Search with Solution Prediction. In IJCAI. 1177\u20131183. https:\/\/doi.org\/10.24963\/ijcai.2020\/164 10.24963\/ijcai.2020\/164","DOI":"10.24963\/ijcai.2020"}],"event":{"name":"ISSTA '24: 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","AITO"],"location":"Vienna Austria","acronym":"ISSTA '24"},"container-title":["Proceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3650212.3680337","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3650212.3680337","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:50:07Z","timestamp":1750287007000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3650212.3680337"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,11]]},"references-count":67,"alternative-id":["10.1145\/3650212.3680337","10.1145\/3650212"],"URL":"https:\/\/doi.org\/10.1145\/3650212.3680337","relation":{},"subject":[],"published":{"date-parts":[[2024,9,11]]},"assertion":[{"value":"2024-09-11","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}