Back to results

Virginia Tech

Constraint-Based Thread-Modular Abstract Interpretation

Abstract

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.

Degree

thesis:*
Name thesis:degree_name
Ph. D.
Level thesis:degree_level
doctoral
Discipline thesis:degree_discipline
Computer Engineering
Department dc:contributor.department
Electrical and Computer Engineering
Grantor dc:publisher
Virginia Tech
Year dc:date.issued
2018

Author and committee

dc:creator, dc:contributor.*
Author dc:creator
  • Kusano, Markus Jan Urban
Chairs dc:contributor.committeechair
  • Wang, Chao
  • Hsiao, Michael S.
Committee members dc:contributor.committeemember
  • Zeng, Haibo
  • Lee, Dongyoon
  • Schaumont, Patrick R.

Subjects

dc:subject × 4

Rights

dc:rights
Statement dc:rights
  • In Copyright

Identifiers

dc:identifier.*
Dc Identifier Other
vt_gsexam:15155
OAI identifier oai:identifier
oai:vtechworks.lib.vt.edu:10919/84399

Chain of custody

source
Harvested from
Virginia Tech
Base URL
vtechworks.lib.vt.edu/oai/request
Last updated
2026-07-22
Source record
OAI-PMH GetRecord
citation

Kusano, Markus Jan Urban. Constraint-Based Thread-Modular Abstract Interpretation. doctoral thesis, Virginia Tech, 2018. http://hdl.handle.net/10919/84399