Due to the complexity of current software and the rising requirements on its reliability, traditional testing no longer suffices to assure the needed quality, and automated analysis and verification methods are needed. However, despite a lot of recent progress in this area, the current methods are still lacking in scalability, precision, and/or capabilities of analysing complex properties of advanced code. This is exactly what the project aims to attack, concentrating on several complementary types of program constructions that are particularly problematic for current automated analyses: namely, low-level pointer operations, dealing with arrays and strings, and concurrency. Both static approaches based on abstract interpretation and model checking as well as dynamic analysis based on extrapolation and noise injection will be studied. In the former case, a special attention will be devoted to approaches based on SAT/SMT solving, including improvements of the decision procedures used.

The goal of the project is to significantly improve state-of-the-art techniques of automated analysis and verification to make them more scalable and applicable for handling more complex properties of more complex code with low-level pointer operations, arrays, strings, and/or concurrency.

P. Parízek, F. Kliber:
Checking Just Pairs of Threads for Efficient and Scalable Incremental Verification of Multithreaded Programs, in Proceedings of JPF Workshop 2022, pp. 27-31, 2023
DOI: 10.1145/3573074.3573082
P. Parízek, F. Kliber:
Incremental Verification of Multithreaded Programs by Checking Interleavings for Pairs of Threads, Technical report no. D3S-TR-2022-01, Department of Distributed and Dependable Systems, Charles University, pp. 1-15, 2022
R. Husák, J. Míšek, F. Zavoral, J. Kofroň:
PeachPie: Mature PHP to CLI compiler, in Journal of Computer Languages, pp. 1-29, 2022
DOI: 10.1016/j.cola.2022.101152
L. Alt, M. Blicha, A. Hyvärinen, N. Sharygina:
SolCMC: Solidity Compiler’s Model Checker, in Computer Aided Verification, pp. 325-338, 2022
ISBN: 978-3-031-13185-1, DOI: 10.1007/978-3-031-13185-1_16
M. Blicha, G. Fedyukovich, A. Hyvärinen, N. Sharygina:
Split Transition Power Abstraction for Unbounded Safety, in Proceedings of FMCAD'22, pp. 349-358, 2022
ISBN: 978-3-85448-053-2, DOI: 10.34727/2022/isbn.978-3-85448-053-2_42
M. Blicha, J. Kofroň, W. Tatarko:
Summarization of branching loops, in Proceedings of the 37th ACM/SIGAPP Symposium on Applied Computing, pp. 1808–1816, 2022
ISBN: 978-1-4503-8713-2, DOI: 10.1145/3477314.3507042
M. Blicha, G. Fedyukovich, A. Hyvärinen, N. Sharygina:
Transition Power Abstractions for Deep Counterexample Detection, in Tools and Algorithms for the Construction and Analysis of Systems, pp. 524-542, 2022
ISBN: 978-3-030-99524-9, DOI: 10.1007/978-3-030-99524-9_29
M. Blicha, A. Hyvärinen, J. Kofroň, N. Sharygina:
Using linear algebra in decomposition of Farkas interpolants, in International Journal on Software Tools for Technology Transfer 24(1), pp. 111-125, 2022
DOI: 10.1007/s10009-021-00641-z
R. Husák, J. Kofroň, J. Míšek, F. Zavoral:
Using Procedure Cloning for Performance Optimization of Compiled Dynamic Languages, in Proc. of the 17th International Conference on Software Technologies, pp. 175-186, 2022
ISBN: 978-989-758-588-3, DOI: 10.5220/0011272300003266
S. Asadi, M. Blicha, A. Hyvärinen, G. Fedyukovich, N. Sharygina:
Farkas-Based Tree Interpolation, in Static Analysis, pp. 357-379, 2020
ISBN: 978-3-030-65474-0, DOI: 10.1007/978-3-030-65474-0_16
S. Asadi, M. Blicha, A. Hyvärinen, G. Fedyukovich, N. Sharygina:
Incremental Verification by SMT-based Summary Repair, in Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020, 2020
ISBN: 978-3-85448-042-6, DOI: 10.34727/2020/isbn.978-3-85448-042-6
Project data
Duration: 2020-2022
Funding body: Czech Science Foundation
ID: 20-07487S
Contact: Jan Kofroň