{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T07:58:22Z","timestamp":1790927902316,"version":"4.1.0"},"publisher-location":"New York, NY, USA","reference-count":80,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,4,12]],"date-time":"2024-04-12T00:00:00Z","timestamp":1712880000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Luxembourg National Research Funds (FNR)","award":["C19\/IS\/13646587\/RASoRS"],"award-info":[{"award-number":["C19\/IS\/13646587\/RASoRS"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,4,12]]},"DOI":"10.1145\/3597503.3639087","type":"proceedings-article","created":{"date-parts":[[2024,4,12]],"date-time":"2024-04-12T16:43:26Z","timestamp":1712940206000},"page":"1-13","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["SpecBCFuzz: Fuzzing LTL Solvers with Boundary Conditions"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0002-1915-3720","authenticated-orcid":false,"given":"Luiz","family":"Carvalho","sequence":"first","affiliation":[{"name":"SnT, University of Luxembourg, Luxembourg, Luxembourg"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1611-3969","authenticated-orcid":false,"given":"Renzo","family":"Degiovanni","sequence":"additional","affiliation":[{"name":"SnT, University of Luxembourg, Luxembourg, Luxembourg"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8312-1358","authenticated-orcid":false,"given":"Maxime","family":"Cordy","sequence":"additional","affiliation":[{"name":"SnT, University of Luxembourg, Luxembourg, Luxembourg"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0532-5296","authenticated-orcid":false,"given":"Nazareno","family":"Aguirre","sequence":"additional","affiliation":[{"name":"University of Rio Cuarto, Rio Cuarto, Argentina"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1045-4861","authenticated-orcid":false,"given":"Yves","family":"Le Traon","sequence":"additional","affiliation":[{"name":"University of Luxembourg, Luxembourg, Luxembourg"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1852-2547","authenticated-orcid":false,"given":"Mike","family":"Papadakis","sequence":"additional","affiliation":[{"name":"University of Luxembourg, Luxembourg, Luxembourg"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,4,12]]},"reference":[{"key":"e_1_3_2_1_1_1","first-page":"26","volume-title":"FMCAD 2013","author":"Alur Rajeev","year":"2013","unstructured":"Rajeev Alur, Salar Moarref, and Ufuk Topcu. Counter-strategy guided refinement of GR(1) temporal logic specifications. In Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20--23, 2013, pages 26--33, 2013."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/1355340"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985795"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-16722-6_23"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37057-1_11"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/646483.691738"},{"key":"e_1_3_2_1_9_1","volume-title":"Hotfuzz: Discovering temporal and spatial denial-of-service vulnerabilities through guided micro-fuzzing. ACM Trans. Priv. Secur., 25(4), jul","author":"Blair William","year":"2022","unstructured":"William Blair, Andrea Mambretti, Sajjad Arshad, Michael Weissbacher, William Robertson, Engin Kirda, and Manuel Egele. Hotfuzz: Discovering temporal and spatial denial-of-service vulnerabilities through guided micro-fuzzing. ACM Trans. Priv. Secur., 25(4), jul 2022."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54013-4_1"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_6"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134020"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3583131.3590454"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14186-7_6"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3377811.3380398"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2017.2785841"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30826-0_1"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2020.3037780"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_29"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45988-X_5"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/646821.706736"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"e_1_3_2_1_23_1","volume-title":"Another look at LTL model checking","author":"Clarke E.","year":"1997","unstructured":"E. Clarke, Orna Grumberg, and Kiyoharu Hamaguchi. Another look at LTL model checking. 1997."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011276507260"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/TEVC.2013.2281535"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180261"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3238220"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2970276.2970349"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"e_1_3_2_1_31_1","volume-title":"ICSE","author":"Maolin","year":"2023","unstructured":"Maolin Sun et al. Validating smt solvers via skeleton enumeration empowered by historical bug-triggering inputs. In ICSE, 2023."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-04921-2_29"},{"key":"e_1_3_2_1_33_1","volume-title":"Proceedings of the 14th USENIX Conference on Offensive Technologies, WOOT'20, USA","author":"Fioraldi Andrea","year":"2020","unstructured":"Andrea Fioraldi, Dominik Maier, Heiko Ei\u00dffeldt, and Marc Heuse. Afl++: Combining incremental steps of fuzzing research. In Proceedings of the 14th USENIX Conference on Offensive Technologies, WOOT'20, USA, 2020. USENIX Association."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(79)90046-1"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_14"},{"key":"e_1_3_2_1_36_1","unstructured":"Luca Geatti Nicola Gigante and Angelo Montanari. BLACK: A fast flexible and reliable LTL satisfiability checker. In Dario Della Monica Gian Luca Pozzato and Enrico Scala editors Proceedings of the 3rd Workshop on Artificial Intelligence and Formal Verification Logic Automata and Synthesis hosted by the Twelfth International Symposium on Games Automata Logics and Formal Verification (GandALF 2021) Padua Italy September 22 2021 volume 2987 of CEUR Workshop Proceedings pages 7--12. CEUR-WS.org 2021."},{"key":"e_1_3_2_1_37_1","first-page":"1","volume-title":"28th International Symposium on Temporal Representation and Reasoning, TIME 2021, September 27--29","volume":"206","author":"Geatti Luca","year":"2021","unstructured":"Luca Geatti, Nicola Gigante, Angelo Montanari, and Gabriele Venturato. Past matters: Supporting ltl+past in the BLACK satisfiability checker. In Carlo Combi, Johann Eder, and Mark Reynolds, editors, 28th International Symposium on Temporal Representation and Reasoning, TIME 2021, September 27--29, 2021, Klagenfurt, Austria, volume 206 of LIPIcs, pages 8:1--8:17. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 2021."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2001.989841"},{"key":"e_1_3_2_1_39_1","volume-title":"9th International Conference on Learning Representations, ICLR 2021","author":"Hahn Christopher","year":"2021","unstructured":"Christopher Hahn, Frederik Schmitt, Jens U. Kreber, Markus Norman Rabe, and Bernd Finkbeiner. Teaching temporal logics to neural networks. In 9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, May 3--7, 2021. OpenReview.net, 2021."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3460319.3464795"},{"key":"e_1_3_2_1_41_1","volume-title":"Spin Model Checker, the: Primer and Reference Manual","author":"Holzmann Gerard","year":"2003","unstructured":"Gerard Holzmann. Spin Model Checker, the: Primer and Reference Manual. Addison-Wesley Professional, first edition, 2003."},{"key":"e_1_3_2_1_42_1","volume-title":"ICSE","author":"Jongwook Kim Hakjoo Oh","year":"2023","unstructured":"Hakjoo Oh Jongwook Kim, Sunbeom So. Diver: Oracle-guided smt solver testing with unrestricted random mutations. In ICSE, 2023."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3424307"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE48619.2023.00187"},{"key":"e_1_3_2_1_45_1","volume-title":"IEE Proceedings E, 130(1):1+","author":"Kramer J.","year":"1983","unstructured":"J. Kramer, J. Magee, M. Sloman, and A. Lister. CONIC: an integrated approach to distributed computer control systems. Computers and Digital Techniques, IEE Proceedings E, 130(1):1+, 1983."},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-01090-4_34"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/333979.333987"},{"key":"e_1_3_2_1_48_1","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","author":"Lamport Leslie","year":"2002","unstructured":"Leslie Lamport. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc., USA, 2002."},{"key":"e_1_3_2_1_49_1","first-page":"186","volume-title":"5th International Conference, FMCAD 2004, Austin, Texas, USA, November 15--17, 2004","author":"Latvala Timo","year":"2004","unstructured":"Timo Latvala, Armin Biere, Keijo Heljanko, and Tommi A. Junttila. Simple bounded LTL model checking. In Formal Methods in Computer-Aided Design, 5th International Conference, FMCAD 2004, Austin, Texas, USA, November 15--17, 2004, Proceedings, pages 186--200, 2004."},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIME.2013.19"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-26287-1_13"},{"key":"e_1_3_2_1_52_1","volume-title":"Quality evaluation of solution sets in multiobjective optimisation: A survey. ACM Comput. Surv., 52(2), mar","author":"Li Miqing","year":"2019","unstructured":"Miqing Li and Xin Yao. Quality evaluation of solution sets in multiobjective optimisation: A survey. ACM Comput. Surv., 52(2), mar 2019."},{"key":"e_1_3_2_1_53_1","first-page":"3292","volume-title":"Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI-22","author":"Luo Weilin","year":"2022","unstructured":"Weilin Luo, Hai Wan, Jianfeng Du, Xiaoda Li, Yuze Fu, Rongzhen Ye, and Delong Zhang. Teaching ltlf satisfiability checking to neural networks. In Lud De Raedt, editor, Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI-22, pages 3292--3298. International Joint Conferences on Artificial Intelligence Organization, 7 2022. Main Track."},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE43902.2021.00132"},{"key":"e_1_3_2_1_55_1","volume-title":"Proceedings of the 37th IEEE\/ACM International Conference on Automated Software Engineering, ASE '22","author":"Luo Weilin","year":"2023","unstructured":"Weilin Luo, Hai Wan, Delong Zhang, Jianfeng Du, and Hengdi Su. Checking ltl satisfiability via end-to-end learning. In Proceedings of the 37th IEEE\/ACM International Conference on Automated Software Engineering, ASE '22, New York, NY, USA, 2023. Association for Computing Machinery."},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3368089.3409763"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_15"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3510003.3510082"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/96267.96279"},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/3460319.3469077"},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/2739482.2768462"},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293882.3339002"},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293882.3330576"},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2017.23404"},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.226.20"},{"key":"e_1_3_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-010-0140-3"},{"key":"e_1_3_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24372-1_28"},{"key":"e_1_3_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-69778-0_28"},{"key":"e_1_3_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02777-2_24"},{"key":"e_1_3_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/3540250.3549139"},{"key":"e_1_3_2_1_72_1","volume-title":"Proceedings of the ACM\/IEEE 45th International Conference on Software Engineering, ICSE '23","author":"Sun Maolin","year":"2023","unstructured":"Maolin Sun, Yibiao Yang, Ming Wen, Yongcong Wang, Yuming Zhou, and Hai Jin. Diver: Oracle-guided smt solver testing with unrestricted random mutations. In Proceedings of the ACM\/IEEE 45th International Conference on Software Engineering, ICSE '23, 2023."},{"key":"e_1_3_2_1_73_1","volume-title":"Requirements Engineering - From System Goals to UML Models to Software Specifications","author":"van Lamsweerde Axel","year":"2009","unstructured":"Axel van Lamsweerde. Requirements Engineering - From System Goals to UML Models to Software Specifications. Wiley, 2009."},{"key":"e_1_3_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.730542"},{"key":"e_1_3_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60915-6_6"},{"key":"e_1_3_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2000.873645"},{"key":"e_1_3_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1145\/3573074.3573083"},{"issue":"110","key":"e_1_3_2_1_78_1","first-page":"119","article-title":"The tableau method for temporal logic: An overview","volume":"28","author":"Wolper Pierre","year":"1985","unstructured":"Pierre Wolper. The tableau method for temporal logic: An overview. Logique et Analyse, 28(110\/111):119--136, 1985.","journal-title":"Logique et Analyse"},{"key":"e_1_3_2_1_79_1","volume-title":"The Fuzzing Book","author":"Zeller Andreas","year":"2023","unstructured":"Andreas Zeller, Rahul Gopinath, Marcel B\u00f6hme, Gordon Fraser, and Christian Holler. Probabilistic grammar fuzzing. In The Fuzzing Book. CISPA Helmholtz Center for Information Security, 2023. Retrieved 2023-01-07 15:01:16+01:00."},{"key":"e_1_3_2_1_80_1","volume-title":"Fuzzing: A survey for roadmap. ACM Comput. Surv., 54(11s), sep","author":"Zhu Xiaogang","year":"2022","unstructured":"Xiaogang Zhu, Sheng Wen, Seyit Camtepe, and Yang Xiang. Fuzzing: A survey for roadmap. ACM Comput. Surv., 54(11s), sep 2022."}],"event":{"name":"ICSE '24: IEEE\/ACM 46th International Conference on Software Engineering","location":"Lisbon Portugal","acronym":"ICSE '24","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","IEEE CS","Faculty of Engineering of University of Porto"]},"container-title":["Proceedings of the IEEE\/ACM 46th International Conference on Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3597503.3639087","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3597503.3639087","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:49:11Z","timestamp":1750286951000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3597503.3639087"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,12]]},"references-count":80,"alternative-id":["10.1145\/3597503.3639087","10.1145\/3597503"],"URL":"https:\/\/doi.org\/10.1145\/3597503.3639087","relation":{},"subject":[],"published":{"date-parts":[[2024,4,12]]},"assertion":[{"value":"2024-04-12","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}