Control Explicit-Data Symbolic Model Checking

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F16%3A00088090" target="_blank" >RIV/00216224:14330/16:00088090 - isvavai.cz</a>
Result on the web
<a href="http://dx.doi.org/10.1145/2888393" target="_blank" >http://dx.doi.org/10.1145/2888393</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1145/2888393" target="_blank" >10.1145/2888393</a>

Result language
angličtina
Original language name
Control Explicit-Data Symbolic Model Checking
Original language description
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.
Czech name
—
Czech description
—

Type
J<sub>x</sub> - Unclassified - Peer-reviewed scientific article (Jimp, Jsc and Jost)
CEP classification
IN - Informatics
OECD FORD branch
—

Project
<a href="/en/project/GA15-08772S" target="_blank" >GA15-08772S: Correctness Analysis of C and C++ Programs with Threads</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Publication year
2016
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Similar results(10)