Control Explicit-Data Symbolic Model Checking

J 2016

Control Explicit-Data Symbolic Model Checking

BAUCH, Petr, Vojtěch HAVEL a Jiří BARNAT

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

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

Utajení

není předmětem státního či obchodního tajemství

Odkazy

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ěněno: 23. 8. 2016 11:04, prof. RNDr. Jiří Barnat, Ph.D.

Anotace

V originále

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 VaV

Název: Analýza korektnosti vícevláknových programů v C a C++

Investor: Grantová agentura ČR, Correctness Analysis of C and C++ Programs with Threads

Citovat

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. Dostupné z: https://dx.doi.org/10.1145/2888393.

@article{1352219,
   author = {Bauch, Petr and Havel, Vojtěch and Barnat, Jiří},
   article_number = {2},
   doi = {http://dx.doi.org/10.1145/2888393},
   keywords = {formal methods; model checking; static analysis; modular arithmetic},
   language = {eng},
   issn = {1049-331X},
   journal = {ACM Transactions on Software Engineering and Methodology},
   title = {Control Explicit-Data Symbolic Model Checking},
   url = {http://doi.acm.org/10.1145/2888393},
   volume = {25},
   year = {2016}
}

TY  - JOUR
ID  - 1352219
AU  - Bauch, Petr - Havel, Vojtěch - Barnat, Jiří
PY  - 2016
TI  - Control Explicit-Data Symbolic Model Checking
JF  - ACM Transactions on Software Engineering and Methodology
VL  - 25
IS  - 2
SP  - 15-62
EP  - 15-62
SN  - 1049331X
KW  - formal methods
KW  - model checking
KW  - static analysis
KW  - modular arithmetic
UR  - http://doi.acm.org/10.1145/2888393
N2  - 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.
ER  -

BAUCH, Petr, Vojtěch HAVEL a Jiří BARNAT. Control Explicit-Data Symbolic Model Checking. \textit{ACM Transactions on Software Engineering and Methodology}. 2016, roč.~25, č.~2, s.~15-62. ISSN~1049-331X. Dostupné z: https://dx.doi.org/10.1145/2888393.

Podrobný výpis o publikaci