Hybrid Partial Order Reduction with Under-Approximate Dynamic Points-To and Determinacy Information

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F16%3A10326885" target="_blank" >RIV/00216208:11320/16:10326885 - isvavai.cz</a>
Result on the web
<a href="http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD16/proceedings/fmcad-2016-proceedings.pdf" target="_blank" >http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD16/proceedings/fmcad-2016-proceedings.pdf</a>
DOI - Digital Object Identifier
—

Result language
angličtina
Original language name
Hybrid Partial Order Reduction with Under-Approximate Dynamic Points-To and Determinacy Information
Original language description
Verification techniques for concurrent systems are often based on systematic state space traversal. An important piece of such techniques is partial order reduction (POR). Many algorithms of POR have been already developed, each having specific advantages and drawbacks. For example, fully dynamic POR is very precise but it has to check every pair of visible actions to detect all interferences. Approaches involving static analysis can exploit knowledge about future behavior of program threads, but they have limited precision. We present a new hybrid POR algorithm that builds upon (i) dynamic POR and (ii) hybrid field access analysis that combines static analysis with data taken on-the-fly from dynamic program states. The key feature of our algorithm is usage of under-approximate dynamic points-to and determinacy information, which is gradually refined during a run of the state space traversal procedure. Knowledge of dynamic points-to sets for local variables improves precision of the field access analysis. Our experimental results show that the proposed hybrid POR achieves better performance than existing techniques on selected benchmarks, and it enables fast detection of concurrency errors.
Czech name
—
Czech description
—

Project
<a href="/en/project/GA14-11384S" target="_blank" >GA14-11384S: Automatic Formal Analysis and Verification of Programs with Complex Unbounded Data and Control Structures</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ů

Article name in the collection
Proceedings of the 16th Conference on Formal Methods in Computer-Aided Design (FMCAD 2016)
ISBN
978-0-9835678-6-8
ISSN
—
e-ISSN
—
Number of pages
8
Pages from-to
141-148
Publisher name
IEEE
Place of publication
Mountain View, CA, USA
Event location
Mountain View, CA, USA
Event date
Oct 3, 2016
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—

Similar results(10)