BAUCH, Petr, Vojtěch HAVEL a Jiří BARNAT. Control Explicit-Data Symbolic Model Checking. ACM Transactions on Software Engineering and Methodology, 2016, roč. 25, č. 2, s. 15-62. ISSN 1049-331X. doi:10.1145/2888393.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Control Explicit-Data Symbolic Model Checking
Autoři BAUCH, Petr (203 Česká republika, domácí), Vojtěch HAVEL (203 Česká republika, domácí) a Jiří BARNAT (203 Česká republika, garant, domácí).
Vydání ACM Transactions on Software Engineering and Methodology, 2016, 1049-331X.
Další údaje
Originální jazyk angličtina
Typ výsledku Článek v odborném periodiku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Spojené státy americké
Utajení není předmětem státního či obchodního tajemství
WWW URL
Impakt faktor Impact factor: 2.516
Kód RIV RIV/00216224:14330/16:00088090
Organizační jednotka Fakulta informatiky
Doi http://dx.doi.org/10.1145/2888393
UT WoS 000377289000005
Klíčová slova anglicky formal methods; model checking; static analysis; modular arithmetic
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: prof. RNDr. Jiří Barnat, Ph.D., učo 3496. Změněno: 23. 8. 2016 11:04.
Anotace
Automatic verification of programs and computer systems with data nondeterminism (e.g., reading from user input) represents a significant and well-motivated challenge. The case of parallel programs is especially difficult, because then also the control flow nontrivially complicates the verification process. We apply the techniques of explicit-state model checking to account for the control aspects of a program to be verified and use set-based reduction of the data flow, thus handling the two sources of nondeterminism separately. We build the theory of set-based reduction using first-order formulae in the bit-vector theory to encode the sets of variable evaluations representing program data. These representations are tested for emptiness and equality (state matching) during the verification, and we harness modern satisfiability modulo theory solvers to implement these tests. We design two methods of implementing the state matching, one using quantifiers and one that is quantifier-free, and we provide both analytical and experimental comparisons. Further experiments evaluate the efficiency of the set-based reduction method, showing the classical, explicit approach to fail to scale with the size of data domains. Finally, we propose and evaluate two heuristics to decrease the number of expensive satisfiability queries, together yielding a 10-fold speedup.
Návaznosti
GA15-08772S, projekt VaVNázev: Analýza korektnosti vícevláknových programů v C a C++
Investor: Grantová agentura ČR, Standardní projekty
VytisknoutZobrazeno: 21. 1. 2020 03:21