Automated software verification and bug hunting are a hot topic in both industry and academia. Indeed, they can save a lot of money and, in case of safety-critical software, even human lives. This project aims at new automated methods of static formal verification (based on approaches like symbolic verification or automated abstraction) as well as extrapolating dynamic analysis and advanced testing of programs that use several classes of advanced programming constructions. In particular, the project concentrates on pointer programs, concurrent programs (including cloud programs), and container programs. While these areas are to some degree independent, there is also a lot of overlap among them: On the one hand, one needs to consider various combinations of the mentioned constructions (e.g., concurrent pointer programs). On the other hand, one needs to solve similar problems for all of them. An important example of the latter considered in the project is dealing with open programs, i.e., program fragments that the programmers need to verify despite their environment is unknown.

The goal of the project is to develop new methods of automated static formal verification (based on approaches like symbolic verification or abstraction) as well as extrapolating dynamic analysis and testing for advanced programs using pointers, concurrency (including the cloud), and/or containers.

Link bibtex
P. Arcaini, A. Gargantini, E. Riccobene:
Decomposition-Based Approach for Model-Based Test Generation, in IEEE Transactions on Software Engineering 45(5), pp. 507-520, 2019
DOI: 10.1109/TSE.2017.2781231
Link bibtex
P. Arcaini, J. Kofroň, P. Ježek:
Validation of the Hybrid ERTMS/ETCS Level 3 using Spin, in International Journal on Software Tools for Technology Transfer, 2019
DOI: 10.1007/s10009-019-00539-x
Link bibtex
P. Arcaini, S. Bonfanti, A. Gargantini, A. Mashkoor, E. Riccobene:
Integrating formal methods into medical software development: The ASM approach, in Science of Computer Programming 158(0), pp. 148-167, 2018
DOI: 10.1016/j.scico.2017.07.003
Link bibtex
M. Kellogg, V. Dort, S. Millstein, M. Ernst:
Lightweight verification of array indexing, in Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2018, pp. 3-14, 2018
ISBN: 978-1-4503-5699-2, DOI: 10.1145/3213846.3213849
Link bibtex
P. Arcaini, A. Gargantini, M. Radavelli:
An Evolutionary Process for Product-driven Updates of Feature Models, in Proceedings of the 12th International Workshop on Variability Modelling of Software-Intensive Systems, pp. 67–74, 2018
ISBN: 978-1-4503-5398-4, DOI: 10.1145/3168365.3168374
Link bibtex
P. Arcaini, A. Gargantini, E. Riccobene:
Fault-based test generation for regular expressions by mutation, in Software Testing, Verification and Reliability 0(0), pp. e1664, 2018
DOI: 10.1002/stvr.1664
Link bibtex
P. Arcaini, P. Ježek, J. Kofroň:
Modelling the Hybrid ERTMS/ETCS Level 3 Case Study in Spin, in Abstract State Machines, Alloy, B, TLA, VDM, and Z, pp. 277-291, 2018
ISBN: 978-3-319-91271-4, DOI: 10.1007/978-3-319-91271-4_19
Link bibtex
P. Arcaini, A. Gargantini, E. Riccobene:
MutRex: A Mutation-Based Generator of Fault Detecting Strings for Regular Expressions, in International Conference on Software Testing, Verification and Validation Workshops, pp. 87-96, 2017
ISBN: 978-1-5090-6676-6, DOI: 10.1109/ICSTW.2017.23
Link bibtex
P. Arcaini, A. Gargantini, P. Vavassori:
Automated Repairing of Variability Models, in Proceedings of the 21st International Systems and Software Product Line Conference - Volume A, pp. 9–18, 2017
ISBN: 978-1-4503-5221-5, DOI: 10.1145/3106195.3106206
Link bibtex
P. Arcaini, E. Riccobene, P. Scandurra:
Formal Design and Verification of Self-Adaptive Systems with Decentralized Control, in ACM Transactions on Autonomous and Adaptive Systems 11(4), pp. 25:1–25:35, 2017
DOI: 10.1145/3019598
Link bibtex
P. Arcaini, A. Gargantini, E. Riccobene:
NuSeen: A Tool Framework for the NuSMV Model Checker, in Intl. Conf. on Software Testing, Verification and Validation (ICST), pp. 476-483, 2017
ISBN: 978-1-5090-6031-3, DOI: 10.1109/ICST.2017.54
Project data
Duration: 2017-2019
Funding body: Czech Science Foundation
ID: 17-12465S
Contact: Jan Kofroň