Control Explicit-Data Symbolic Model Checking

Kód výsledku v 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>

Výsledek na webu

<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>

Jazyk výsledku

angličtina

Název v původním jazyce

Control Explicit-Data Symbolic Model Checking

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Control Explicit-Data Symbolic Model Checking

Popis výsledku anglicky

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.

Druh

J_x - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

<a href="/cs/project/GA15-08772S" target="_blank" >GA15-08772S: Analýza korektnosti vícevláknových programů v C a C++</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2016

Kód důvěrnosti údajů

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

Název periodika

ACM Transactions on Software Engineering and Methodology

ISSN

1049-331X

e-ISSN

—

Svazek periodika

25

Číslo periodika v rámci svazku

2

Stát vydavatele periodika

US - Spojené státy americké

Počet stran výsledku

48

Strana od-do

15-62

Kód UT WoS článku

000377289000005

EID výsledku v databázi Scopus

—