DARTS.10.2.5.pdf
- Filesize: 0.7 MB
- 5 pages
Document
Mutation-Based Lifted Repair of Software Product Lines (Artifact)
Author
Aleksandar S. Dimovski 
-
Part of:
Issue:
Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024)
Volume: DARTS, Volume 10 (ECOOP 2024)
Conference: European Conference on Object-Oriented Programming (ECOOP)
Journal: Dagstuhl Artifacts Series (DARTS) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2024-09-12
Artifact Description
Document Identifiers
Author Details
Cite AsGet BibTex
Aleksandar S. Dimovski. Mutation-Based Lifted Repair of Software Product Lines (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 5:1-5:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/DARTS.10.2.5
https://doi.org/10.4230/DARTS.10.2.5
Artifact
DARTS-10-2-5-artifact-f2ecaff1a457cd1f62a152186750634e.ova
(Filesize: 9.37 GB)
Artifact Evaluation Policy
The artifact has been evaluated as described in the ECOOP 2024 Call for Artifacts and the ACM Artifact Review and Badging Policy.
Abstract
In this work, we describe the installation, usage, and evaluation results of the tool SPLAllRepair, which is introduced by the paper "Mutation-based Lifted Repair of Software Product Lines". We provide step-by-step instructions on how to download, run, and compare the tool’s outputs to outputs described in the paper. The tool implements a novel lifted repair algorithm for program families (Software Product Lines - SPLs) based on code mutations. The inputs of our algorithm are an erroneous SPL and a specification given in the form of assertions. We use variability encoding to transform the given SPL into a single program, called family simulator, which is translated into a set of SMT formulas whose conjunction is satisfiable iff the simulator (i.e. the input SPL) violates an assertion. We use a predefined set of mutations applied to feature and program expressions of the given SPL. The algorithm repeatedly mutates the erroneous family simulator and checks if it becomes (bounded) correct. The outputs are all minimal repairs in the form of minimal number of (feature and program) expression replacements such that the repaired SPL is (bounded) correct with respect to a given set of assertions. We present the experimental results showing that our approach is able to successfully repair various interesting #ifdef-based C SPLs.
Subject Classification
ACM Subject Classification
- Software and its engineering → Software product lines
- Theory of computation → Abstraction
Keywords
- Program repair
- Software Product Lines
- Code mutations
- Variability encoding
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Edmund M. Clarke, Daniel Kroening, and Flavio Lerda. A tool for checking ANSI-C programs. In Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, Proceedings, volume 2988 of LNCS, pages 168-176. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-24730-2_15.
- Leonardo Mendonça 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, 14th International Conference, TACAS 2008. Proceedings, volume 4963 of LNCS, pages 337-340. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-78800-3_24.
-
Aleksandar S. Dimovski. Symbolic game semantics for model checking program families. In Model Checking Software - 23nd International Symposium, SPIN 2016, Proceedings, volume 9641 of LNCS, pages 19-37. Springer, 2016.
- Aleksandar S. Dimovski. Lifted static analysis using a binary decision diagram abstract domain. In Proceedings of the 18th ACM SIGPLAN International Conference on GPCE 2019, pages 102-114. ACM, 2019. URL: https://doi.org/10.1145/3357765.3359518.
- Aleksandar S. Dimovski. Ctl^⋆ family-based model checking using variability abstractions and modal transition systems. Int. J. Softw. Tools Technol. Transf., 22(1):35-55, 2020. URL: https://doi.org/10.1007/s10009-019-00528-0.
- Aleksandar S. Dimovski. Mutation-based lifted repair of software product lines. In 38th European Conference on Object-Oriented Programming, ECOOP 2024, volume 313 of LIPIcs, pages 36:1-36:24. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2024.36.
- Aleksandar S. Dimovski. Tool artifact for "mutation-based lifted repair of software product lines". Zenodo, 2024. URL: https://doi.org/10.5281/zenodo.12588017.
- Aleksandar S. Dimovski, Sven Apel, and Axel Legay. Several lifted abstract domains for static analysis of numerical program families. Sci. Comput. Program., 213:102725, 2022. URL: https://doi.org/10.1016/J.SCICO.2021.102725.
- Aleksandar S. Dimovski and Andrzej Wasowski. From transition systems to variability models and from lifted model checking back to UPPAAL. In Models, Algorithms, Logics and Tools, volume 10460 of LNCS, pages 249-268. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-63121-9_13.
- Mark H. Liffiton and Jordyn C. Maglalang. A cardinality solver: More expressive constraints for free - (poster presentation). In Theory and Applications of Satisfiability Testing - SAT 2012 - 15th Int. Conf., Proceedings, volume 7317 of LNCS, pages 485-486. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-31612-8_47.
- Bat-Chen Rothenberg and Orna Grumberg. Sound and complete mutation-based program repair. In FM 2016: Formal Methods - 21st International Symposium, Proceedings, volume 9995 of LNCS, pages 593-611, 2016. URL: https://doi.org/10.1007/978-3-319-48989-6_36.