Constraint-Based Thread-Modular Abstract Interpretation
| dc.contributor.author | Kusano, Markus Jan Urban | en |
| dc.contributor.committeechair | Wang, Chao | en |
| dc.contributor.committeechair | Hsiao, Michael S. | en |
| dc.contributor.committeemember | Zeng, Haibo | en |
| dc.contributor.committeemember | Lee, Dongyoon | en |
| dc.contributor.committeemember | Schaumont, Patrick R. | en |
| dc.contributor.department | Electrical and Computer Engineering | en |
| dc.date.accessioned | 2018-07-26T08:00:41Z | en |
| dc.date.available | 2018-07-26T08:00:41Z | en |
| dc.date.issued | 2018-07-25 | en |
| dc.description.abstract | In this dissertation, I present a set of novel constraint-based thread-modular abstract-interpretation techniques for static analysis of concurrent programs. Specifically, I integrate a lightweight constraint solver into a thread-modular abstract interpreter to reason about inter-thread interference more accurately. Then, I show how to extend the new analyzer from programs running on sequentially consistent memory to programs running on weak memory. Finally, I show how to perform incremental abstract interpretation, with and without the previously mentioned constraint solver, by analyzing only regions of the program impacted by a program modification. I also demonstrate, through experiments, that these new constraint-based static analyzers are significantly more accurate than prior abstract interpretation-based static analyzers, with lower runtime overhead, and that the incremental technique can drastically reduce runtime overhead in the presence of small program modifications. | en |
| dc.description.degree | Ph. D. | en |
| dc.format.medium | ETD | en |
| dc.identifier.other | vt_gsexam:15155 | en |
| dc.identifier.uri | http://hdl.handle.net/10919/84399 | en |
| dc.publisher | Virginia Tech | en |
| dc.rights | In Copyright | en |
| dc.rights.uri | http://rightsstatements.org/vocab/InC/1.0/ | en |
| dc.subject | abstract interpretation | en |
| dc.subject | concurrency | en |
| dc.subject | verification | en |
| dc.subject | static analysis | en |
| dc.title | Constraint-Based Thread-Modular Abstract Interpretation | en |
| dc.type | Dissertation | en |
| thesis.degree.discipline | Computer Engineering | en |
| thesis.degree.grantor | Virginia Polytechnic Institute and State University | en |
| thesis.degree.level | doctoral | en |
| thesis.degree.name | Ph. D. | en |
Files
Original bundle
1 - 1 of 1