Type
Text
Type
Dissertation
Advisor
Scott D. Stoller | Qin, Hong | Klaus Havelund.
Date
2010-12-01
Keywords
Computer Science | Compiler, Model Checking, Runtime Verification
Department
Department of Computer Science
Language
en_US
Source
This work is sponsored by the Stony Brook University Graduate School in compliance with the requirements for completion of degree.
Identifier
http://hdl.handle.net/11401/72544
Publisher
The Graduate School, Stony Brook University: Stony Brook, NY.
Format
application/pdf
Abstract
In this dissertation we present a compiler-assisted execution-based software modelchecking method targeting all languages that are acceptable by the compiler. We treatthe intermediate representation of the program under compilation as a language andinterpret it using a customized virtual machine. Our model checkers are based on thisintermediate representation level virtual machine and have full access to its states. Weimplemented two model checkers: a stateless Monte Carlo model checker GMC2 anda bounded concrete-symbolic model checker using the dynamic path reduction algorithmfor reachability problems of linear C programs.We also introduce the new technique of Software Monitoring with Controllable Over-head (SMCO). SMCO is formally grounded in control theory, in particular, the supervi-sory control of discrete event systems. Overhead is controlled by dynamically disablingevent interrupts, but such interrupts are disabled for as short a time as possible so thatthe total number of events monitored, under the constraint of a user-supplied targetoverhead, is maximized.We have implemented SMCO using a technique we call Compiler-Assisted Instrumen-tation (CAI). Benchmark shows that SMCO successfully controls overhead across a widerange of target-overhead levels. Moreover, its accuracy monotonically increases with thetarget overhead, and it can be configured to distribute monitoring overhead fairly acrossmultiple instrumentation points.
Recommended Citation
Huang, Xiaowan, "Compiler-Assisted Software Model Checking and Monitoring" (2010). Stony Brook Theses and Dissertations Collection, 2006-2020 (closed to submissions). 1748.
https://commons.library.stonybrook.edu/stony-brook-theses-and-dissertations-collection/1748