| dc.identifier.uri | http://hdl.handle.net/1951/55475 | |
| dc.identifier.uri | http://hdl.handle.net/11401/72544 | |
| dc.description.sponsorship | This work is sponsored by the Stony Brook University Graduate School in compliance with the requirements for completion of degree. | en_US |
| dc.format | Monograph | |
| dc.format.medium | Electronic Resource | en_US |
| dc.language.iso | en_US | |
| dc.publisher | The Graduate School, Stony Brook University: Stony Brook, NY. | |
| dc.type | Dissertation | |
| dcterms.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. | |
| dcterms.available | 2012-05-15T18:04:09Z | |
| dcterms.available | 2015-04-24T14:52:35Z | |
| dcterms.contributor | Qin, Hong | en_US |
| dcterms.contributor | Scott D. Stoller | en_US |
| dcterms.contributor | Klaus Havelund. | en_US |
| dcterms.creator | Huang, Xiaowan | |
| dcterms.dateAccepted | 2012-05-15T18:04:09Z | |
| dcterms.dateAccepted | 2015-04-24T14:52:35Z | |
| dcterms.dateSubmitted | 2012-05-15T18:04:09Z | |
| dcterms.dateSubmitted | 2015-04-24T14:52:35Z | |
| dcterms.description | Department of Computer Science | en_US |
| dcterms.format | Monograph | |
| dcterms.format | Application/PDF | en_US |
| dcterms.identifier | http://hdl.handle.net/1951/55475 | |
| dcterms.identifier | Huang_grad.sunysb_0771E_10395.pdf | en_US |
| dcterms.identifier | http://hdl.handle.net/11401/72544 | |
| dcterms.issued | 2010-12-01 | |
| dcterms.language | en_US | |
| dcterms.provenance | Made available in DSpace on 2012-05-15T18:04:09Z (GMT). No. of bitstreams: 1
Huang_grad.sunysb_0771E_10395.pdf: 1116342 bytes, checksum: f193975afd47e801c71e2ae0912a87b1 (MD5)
Previous issue date: 1 | en |
| dcterms.provenance | Made available in DSpace on 2015-04-24T14:52:35Z (GMT). No. of bitstreams: 3
Huang_grad.sunysb_0771E_10395.pdf.jpg: 1894 bytes, checksum: a6009c46e6ec8251b348085684cba80d (MD5)
Huang_grad.sunysb_0771E_10395.pdf.txt: 219197 bytes, checksum: 7f606afaca5588e597399fe8815b4c31 (MD5)
Huang_grad.sunysb_0771E_10395.pdf: 1116342 bytes, checksum: f193975afd47e801c71e2ae0912a87b1 (MD5)
Previous issue date: 1 | en |
| dcterms.publisher | The Graduate School, Stony Brook University: Stony Brook, NY. | |
| dcterms.subject | Computer Science | |
| dcterms.subject | Compiler, Model Checking, Runtime Verification | |
| dcterms.title | Compiler-Assisted Software Model Checking and Monitoring | |
| dcterms.type | Dissertation | |
