Cited By
View all- Jovanovic ASullivan A(2024)Mutation testing for temporal alloy models (extended version)Software and Systems Modeling10.1007/s10270-024-01220-xOnline publication date: 28-Oct-2024
SpecBCFuzz: Fuzzing LTL Solvers with Boundary Conditions
Authors: 
Luiz Carvalho, Renzo Degiovanni, Maxime Cordy, Nazareno Aguirre, Yves Le Traon, Mike PapadakisAuthors Info & Claims
Article No.: 123, Pages 1 - 13
Abstract
LTL solvers check the satisfiability of Linear-time Temporal Logic (LTL) formulas and are widely used for verifying and testing critical software systems. Thus, potential bugs in the solvers' implementations can have a significant impact. We present SpecBCFuzz, a fuzzing method for finding bugs in LTL solvers, that is guided by boundary conditions (BCs), corner cases whose (un)satisfiability depends on rare traces. SpecBCFuzz implements a search-based algorithm that fuzzes LTL formulas giving relevance to BCs. It integrates syntactic and semantic similarity metrics to explore the vicinity of the seeded formulas with BCs. We evaluate SpecBCFuzz on 21 different configurations (including the latest and past releases) of four mature and state-of-the-art LTL solvers (NuSMV, Black, Aalta, and PLTL) that implement a diverse set of satisfiability algorithms. SpecBCFuzz produces 368,716 bug-triggering formulas, detecting bugs in 18 out of the 21 solvers' configurations we study. Overall, SpecBCFuzz reveals: soundness issues (wrong answers given by a solver) in Aalta and PLTL; crashes, e.g., segmentation faults, in NuSMV, Black and Aalta; flaky behaviors (different responses across re-runs of the solver on the same formula) in NuSMV and Aalta; performance bugs (large time performance degradation between successive versions of the solver on the same formula) in Black, Aalta and PLTL; and no bug in NuSMV BDD (all versions), suggesting that the latter is currently the most robust solver.
References
[1]
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.
[2]
Paul Ammann and Jeff Offutt. Introduction to Software Testing. Cambridge University Press, 2008.
[3]
Andrea Arcuri and Lionel Briand. A practical guide for using statistical tests to assess randomized algorithms in software engineering. In Proceedings of the 33rd International Conference on Software Engineering, ICSE '11, page 1--10, New York, NY, USA, 2011. Association for Computing Machinery.
[4]
Haniel et al. Barbosa. cvc5: A versatile and industrial-strength smt solver. In Dana Fisman and Grigore Rosu, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 415--442, Cham, 2022. Springer International Publishing.
[5]
Dirk Beyer and Marie-Christine Jakobs. Coveritest: Cooperative verifier-based testing. In Reiner Hähnle and Wil M. P. van der Aalst, editors, Fundamental Approaches to Software Engineering - 22nd International Conference, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6--11, 2019, Proceedings, volume 11424 of Lecture Notes in Computer Science, pages 389--408. Springer, 2019.
[6]
Dirk Beyer and M. Erkan Keremoglu. Cpachecker: A tool for configurable software verification. In Ganesh Gopalakrishnan and Shaz Qadeer, editors, Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14--20, 2011. Proceedings, volume 6806 of Lecture Notes in Computer Science, pages 184--190. Springer, 2011.
[7]
Dirk Beyer and Stefan Löwe. Explicit-state software model checking based on CEGAR and interpolation. In Vittorio Cortellessa and Dániel Varró, editors, Fundamental Approaches to Software Engineering - 16th International Conference, FASE 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16--24, 2013. Proceedings, volume 7793 of Lecture Notes in Computer Science, pages 146--162. Springer, 2013.
[8]
Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Yunshan Zhu. Symbolic model checking without bdds. In Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS '99, page 193--207, Berlin, Heidelberg, 1999. Springer-Verlag.
[9]
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.
[10]
Roderick Bloem, Robert Könighofer, and Martina Seidl. Sat-based synthesis methods for safety specs. In Kenneth L. McMillan and Xavier Rival, editors, Verification, Model Checking, and Abstract Interpretation, pages 1--20, Berlin, Heidelberg, 2014. Springer Berlin Heidelberg.
[11]
Dmitry Blotsky, Federico Mora, Murphy Berzish, Yunhui Zheng, Ifaz Kabir, and Vijay Ganesh. Stringfuzz: A fuzzer for string solvers. In Hana Chockler and Georg Weissenbacher, editors, Computer Aided Verification, pages 45--51, Cham, 2018. Springer International Publishing.
[12]
Marcel Böhme, Van-Thuan Pham, Manh-Dung Nguyen, and Abhik Roychoudhury. Directed greybox fuzzing. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS '17, page 2329--2344, New York, NY, USA, 2017. Association for Computing Machinery.
[13]
Matías Brizzio, Maxime Cordy, Mike Papadakis, César Sánchez, Nazareno Aguirre, and Renzo Degiovanni. Automated repair of unrealisable ltl specifications guided by model counting. In Proceedings of the Genetic and Evolutionary Computation Conference, GECCO '23, page 1499--1507, New York, NY, USA, 2023. Association for Computing Machinery.
[14]
Robert Brummayer, Florian Lonsing, and Armin Biere. Automated testing and debugging of sat and qbf solvers. In Ofer Strichman and Stefan Szeider, editors, Theory and Applications of Satisfiability Testing - SAT 2010, pages 44--57, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg.
[15]
Alexandra Bugariu and Peter Müller. Automatically testing string solvers. In Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering, ICSE '20, page 1459--1470, New York, NY, USA, 2020. Association for Computing Machinery.
[16]
Marcel Böhme, Van-Thuan Pham, and Abhik Roychoudhury. Coverage-based greybox fuzzing as markov chain. IEEE Transactions on Software Engineering, 45(5):489--506, 2019.
[17]
Luiz Carvalho, Renzo Degiovanni, Matías Brizzio, Maxime Cordy, Nazareno Aguirre, Yves Le Traon, and Mike Papadakis. Acore: Automated goal-conflict resolution. In Leen Lambers and Sebastián Uchitel, editors, Fundamental Approaches to Software Engineering, pages 3--25, Cham, 2023. Springer Nature Switzerland.
[18]
Konstantin Chukharev, Dmitrii Suvorov, Daniil Chivilikhin, and Valeriy Vyatkin. Sat-based counterexample-guided inductive synthesis of distributed controllers. IEEE Access, 8:207485--207498, 2020.
[19]
Alessandro Cimatti, Edmund Clarke, Enrico Giunchiglia, Fausto Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, and Armando Tacchella. Nusmv 2: An opensource tool for symbolic model checking. In Ed Brinksma and Kim Guldstrand Larsen, editors, Computer Aided Verification, pages 359--364, Berlin, Heidelberg, 2002. Springer Berlin Heidelberg.
[20]
Alessandro Cimatti, Enrico Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, and Armando Tacchella. Integrating bdd-based and sat-based symbolic model checking. In Alessandro Armando, editor, Frontiers of Combining Systems, pages 49--56, Berlin, Heidelberg, 2002. Springer Berlin Heidelberg.
[21]
Alessandro Cimatti, Enrico Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, and Armando Tacchella. Integrating bdd-based and sat-based symbolic model checking. In Proceedings of the 4th International Workshop on Frontiers of Combining Systems, FroCoS '02, page 49--56, Berlin, Heidelberg, 2002. Springer-Verlag.
[22]
Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, and Roberto Sebastiani. The mathsat5 smt solver. In Nir Piterman and Scott A. Smolka, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 93--107, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg.
[23]
E. Clarke, Orna Grumberg, and Kiyoharu Hamaguchi. Another look at LTL model checking. 1997.
[24]
Edmund Clarke, Armin Biere, Richard Raimi, and Yunshan Zhu. Bounded model checking using satisfiability solving. Formal Methods in System Design, 19:7--34, 01 2001.
[25]
Leonardo de Moura and Nikolaj Bjørner. Z3: An efficient smt solver. In C. R. Ramakrishnan and Jakob Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 337--340, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg.
[26]
Kalyanmoy Deb and Himanshu Jain. An evolutionary many-objective optimization algorithm using reference-point-based nondominated sorting approach, part i: Solving problems with box constraints. IEEE Transactions on Evolutionary Computation, 18(4):577--601, 2014.
[27]
Renzo Degiovanni, Pablo F. Castro, Marcelo Arroyo, Marcelo Ruiz, Nazareno Aguirre, and Marcelo F. Frias. Goal-conflict likelihood assessment based on model counting. In Proceedings of the 40th International Conference on Software Engineering, ICSE 2018, Gothenburg, Sweden, pages 1125--1135, 2018.
[28]
Renzo Degiovanni, Facundo Molina, Germán Regis, and Nazareno Aguirre. A genetic algorithm for goal-conflict identification. In Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, ASE 2018, Montpellier, France, September 3--7, 2018, pages 520--531, 2018.
[29]
Renzo Degiovanni, Nicolás Ricci, Dalal Alrajeh, Pablo F. Castro, and Nazareno Aguirre. Goal-conflict detection based on temporal satisfiability checking. In Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, ASE 2016, Singapore, September 3--7, 2016, pages 507--518, 2016.
[30]
Niklas Eén and Niklas Sörensson. An extensible sat-solver. In Enrico Giunchiglia and Armando Tacchella, editors, Theory and Applications of Satisfiability Testing, pages 502--518, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg.
[31]
Maolin Sun et al. Validating smt solvers via skeleton enumeration empowered by historical bug-triggering inputs. In ICSE, 2023.
[32]
Bernd Finkbeiner and Hazem Torfah. Counting models of linear-time temporal logic. In Adrian Horia Dediu, Carlos Martín-Vide, José Luis Sierra-Rodríguez, and Bianca Truthe, editors, Language and Automata Theory and Applications - 8th International Conference, LATA 2014, Madrid, Spain, March 10--14, 2014. Proceedings, volume 8370 of Lecture Notes in Computer Science, pages 360--371. Springer, 2014.
[33]
Andrea Fioraldi, Dominik Maier, Heiko Eißfeldt, 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.
[34]
Michael J. Fischer and Richard E. Ladner. Propositional dynamic logic of regular programs. Journal of Computer and System Sciences, 18(2):194--211, 1979.
[35]
Sicun Gao, Soonho Kong, and Edmund M. Clarke. dreal: An smt solver for nonlinear theories over the reals. In Maria Paola Bonacina, editor, Automated Deduction - CADE-24, pages 208--214, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg.
[36]
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.
[37]
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ür Informatik, 2021.
[38]
D. Giannakopoulou and K. Havelund. Automata-based verification of temporal properties on running programs. In Proceedings 16th Annual International Conference on Automated Software Engineering (ASE 2001), pages 412--416, 2001.
[39]
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.
[40]
Adrian Herrera, Hendra Gunadi, Shane Magrath, Michael Norrish, Mathias Payer, and Antony L. Hosking. Seed selection for successful fuzzing. In Proceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2021, page 230--243, New York, NY, USA, 2021. Association for Computing Machinery.
[41]
Gerard Holzmann. Spin Model Checker, the: Primer and Reference Manual. Addison-Wesley Professional, first edition, 2003.
[42]
Hakjoo Oh Jongwook Kim, Sunbeom So. Diver: Oracle-guided smt solver testing with unrestricted random mutations. In ICSE, 2023.
[43]
Hong Jin Kang and David Lo. Adversarial specification mining. ACM Trans. Softw. Eng. Methodol., 30(2):16:1--16:40, 2021.
[44]
Jongwook Kim, Sunbeom So, and Hakjoo Oh. 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.
[45]
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.
[46]
Jan Kretínský, Tobias Meggendorfer, and Salomon Sickert. Owl: A library for ω-words, automata, and LTL. In Shuvendu K. Lahiri and Chao Wang, editors, Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7--10, 2018, Proceedings, volume 11138 of Lecture Notes in Computer Science, pages 543--550. Springer, 2018.
[47]
Orna Kupferman, Moshe Y. Vardi, and Pierre Wolper. An automata-theoretic approach to branching-time model checking. J. ACM, 47(2):312--360, mar 2000.
[48]
Leslie Lamport. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc., USA, 2002.
[49]
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.
[50]
Jianwen Li, Lijun Zhang, Geguang Pu, Moshe Y. Vardi, and Jifeng He. Ltl satisfiability checking revisited. In 2013 20th International Symposium on Temporal Representation and Reasoning, pages 91--98, 2013.
[51]
Jianwen Li, Shufang Zhu, Geguang Pu, and Moshe Y. Vardi. Sat-based explicit ltl reasoning. In Nir Piterman, editor, Hardware and Software: Verification and Testing, pages 209--224, Cham, 2015. Springer International Publishing.
[52]
Miqing Li and Xin Yao. Quality evaluation of solution sets in multiobjective optimisation: A survey. ACM Comput. Surv., 52(2), mar 2019.
[53]
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.
[54]
Weilin Luo, Hai Wan, Xiaotong Song, Binhao Yang, Hongzhen Zhong, and Yin Chen. How to identify boundary conditions with contrasty metric? In 43rd IEEE/ACM International Conference on Software Engineering, ICSE 2021, Madrid, Spain, 22--30 May 2021, pages 1473--1484. IEEE, 2021.
[55]
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.
[56]
Zohar Manna and Amir Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag New York, Inc., New York, NY, USA, 1992.
[57]
Muhammad Numair Mansur, Maria Christakis, Valentin Wüstholz, and Fuyuan Zhang. Detecting critical bugs in smt solvers using blackbox mutational fuzzing. In Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2020, page 701--712, New York, NY, USA, 2020. Association for Computing Machinery.
[58]
Will Marrero. Using bdds to decide ctl. In Nicolas Halbwachs and Lenore D. Zuck, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 222--236, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg.
[59]
Ruijie Meng, Zhen Dong, Jialin Li, Ivan Beschastnikh, and Abhik Roychoudhury. Linear-time temporal logic guided greybox fuzzing. In 44th IEEE/ACM 44th International Conference on Software Engineering, ICSE 2022, Pittsburgh, PA, USA, May 25--27, 2022, pages 1343--1355. ACM, 2022.
[60]
Barton P. Miller, Lars Fredriksen, and Bryan So. An empirical study of the reliability of unix utilities. Commun. ACM, 33(12):32--44, dec 1990.
[61]
Roberto Natella and Van-Thuan Pham. Profuzzbench: A benchmark for stateful protocol fuzzing. In Proceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis, 2021.
[62]
Antonio J. Nebro, Juan J. Durillo, and Matthieu Vergne. Redesigning the jmetal multi-objective optimization framework. In Proceedings of the Companion Publication of the 2015 Annual Conference on Genetic and Evolutionary Computation, GECCO Companion '15, page 1093--1100, New York, NY, USA, 2015. Association for Computing Machinery.
[63]
Rohan Padhye, Caroline Lemieux, and Koushik Sen. Jqf: Coverage-guided property-based testing in java. In Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2019, page 398--401, New York, NY, USA, 2019. Association for Computing Machinery.
[64]
Rohan Padhye, Caroline Lemieux, Koushik Sen, Mike Papadakis, and Yves Le Traon. Semantic fuzzing with zest. In Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2019, page 329--340, New York, NY, USA, 2019. Association for Computing Machinery.
[65]
Sanjay Rawat, Vivek Jain, Ashish Kumar, Lucian Cojocar, Cristiano Giuffrida, and Herbert Bos. Vuzzer: Application-aware evolutionary fuzzing. In 24th Annual Network and Distributed System Security Symposium, NDSS 2017, San Diego, California, USA, February 26 - March 1, 2017. The Internet Society, 2017.
[66]
Mark Reynolds. A new rule for ltl tableaux. In International Symposium on Games, Automata, Logics and Formal Verification, 2016.
[67]
Kristin Y. Rozier and Moshe Y. Vardi. LTL satisfiability checking. STTT, 12(2):123--137, 2010.
[68]
Viktor Schuppan and Luthfi Darmawan. Evaluating ltl satisfiability solvers. In Proceedings of the 9th International Conference on Automated Technology for Verification and Analysis, ATVA'11, page 397--413, Berlin, Heidelberg, 2011. SpringerVerlag.
[69]
Stefan Schwendimann. A new one-pass tableau calculus for pltl. In Harrie de Swart, editor, Automated Reasoning with Analytic Tableaux and Related Methods, pages 277--291, Berlin, Heidelberg, 1998. Springer Berlin Heidelberg.
[70]
Mate Soos, Karsten Nohl, and Claude Castelluccia. Extending sat solvers to cryptographic problems. In Oliver Kullmann, editor, Theory and Applications of Satisfiability Testing - SAT 2009, pages 244--257, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg.
[71]
Dominic Steinhöfel and Andreas Zeller. Input invariants. In Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2022, page 583--594, New York, NY, USA, 2022. Association for Computing Machinery.
[72]
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.
[73]
Axel van Lamsweerde. Requirements Engineering - From System Goals to UML Models to Software Specifications. Wiley, 2009.
[74]
Axel van Lamsweerde, Robert Darimont, and Emmanuel Letier. Managing conflicts in goal-driven requirements engineering. IEEE Trans. Software Eng., 24(11):908--926, 1998.
[75]
Moshe Vardi. An automata-theoretic approach to linear temporal logic. Logics for Concurrency, pages 238--266, 1996.
[76]
Willem Visser, Klaus Havelund, Guillaume P. Brat, and Seungjoon Park. Model checking programs. In The Fifteenth IEEE International Conference on Automated Software Engineering, ASE 2000, Grenoble, France, September 11--15, 2000, pages 3--12. IEEE Computer Society, 2000.
[77]
Matt Walker, Parssa Khazra, Anto Nanah Ji, Hongru Wang, and Franck van Breugel. Jpf-logic: A framework for checking temporal logic properties of java code. SIGSOFT Softw. Eng. Notes, 48(1):32--36, jan 2023.
[78]
Pierre Wolper. The tableau method for temporal logic: An overview. Logique et Analyse, 28(110/111):119--136, 1985.
[79]
Andreas Zeller, Rahul Gopinath, Marcel Böhme, 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.
[80]
Xiaogang Zhu, Sheng Wen, Seyit Camtepe, and Yang Xiang. Fuzzing: A survey for roadmap. ACM Comput. Surv., 54(11s), sep 2022.
Recommendations
HornFuzz: Fuzzing CHC solvers
EASE '23: Proceedings of the 27th International Conference on Evaluation and Assessment in Software EngineeringMany advanced program analysis and verification methods are based on solving systems of Constrained Horn Clauses (CHC). Testing CHC solvers is very important, as correctness of their work determines whether bugs in the analyzed programs are detected or ...
Validating SMT Solvers via Skeleton Enumeration Empowered by Historical Bug-Triggering Inputs
ICSE '23: Proceedings of the 45th International Conference on Software EngineeringSMT solvers check the satisfiability of logic formulas over first-order theories, which have been utilized in a rich number of critical applications, such as software verification, test case generation, and program synthesis. Bugs hidden in SMT ...
On the freeze quantifier in Constraint LTL: Decidability and complexity
Constraint LTL, a generalisation of LTL over Presburger constraints, is often used as a formal language to specify the behavior of operational models with constraints. The freeze quantifier can be part of the language, as in some real-time logics, but ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
May 2024
2942 pages
ISBN:9798400702174
DOI:10.1145/3597503
- Co-chairs:
- Ana Paiva,
- Rui Abreu,
- Program Co-chairs:
- Abhik Roychoudhury,
- Margaret Storey
This work is licensed under a Creative Commons Attribution International 4.0 License.
Sponsors
In-Cooperation
- Faculty of Engineering of University of Porto
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 12 April 2024
Check for updates
Author Tags
Qualifiers
- Research-article
Funding Sources
- Luxembourg National Research Funds (FNR)
Conference
ICSE '24
Sponsor:
ICSE '24: IEEE/ACM 46th International Conference on Software Engineering
April 14 - 20, 2024
Lisbon, Portugal
Acceptance Rates
Overall Acceptance Rate 276 of 1,856 submissions, 15%
Upcoming Conference
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 291Total Downloads
- Downloads (Last 12 months)291
- Downloads (Last 6 weeks)68
Reflects downloads up to 13 Dec 2024
Other Metrics
Citations
Cited By
View all- Jovanovic ASullivan A(2024)Mutation testing for temporal alloy models (extended version)Software and Systems Modeling10.1007/s10270-024-01220-xOnline publication date: 28-Oct-2024
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in