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.abstractgeneral | Software touches nearly every aspect of our lives, from smartphones, personal computers, and websites, to airplanes, cars, and medical equipment. Due to its ubiquity, we would like software in our lives to operate correctly, that is, without any unintended side effects, or freezes. This dissertation presents a new technique to automatically analyze a piece of software and determine if it runs as intended. We focus particularly on software where multiple entities run simultaneously, and thus can interact in many ways. Our automated analysis gives software developers high assurance that the software will always perform correctly, and thus never have any unexpected issues. | 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