{"@context":"http://iiif.io/api/presentation/2/context.json","@id":"https://repo.library.stonybrook.edu/cantaloupe/iiif/2/manifest.json","@type":"sc:Manifest","label":"Compiler-Assisted Software Model Checking and Monitoring","metadata":[{"label":"dc.description.sponsorship","value":"This work is sponsored by the Stony Brook University Graduate School in compliance with the requirements for completion of degree."},{"label":"dc.format","value":"Monograph"},{"label":"dc.format.medium","value":"Electronic Resource"},{"label":"dc.identifier.uri","value":"http://hdl.handle.net/1951/55475"},{"label":"dc.language.iso","value":"en_US"},{"label":"dc.publisher","value":"The Graduate School, Stony Brook University: Stony Brook, NY."},{"label":"dcterms.abstract","value":"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."},{"label":"dcterms.available","value":"2012-05-15T18:04:09Z"},{"label":"dcterms.contributor","value":"Qin, Hong"},{"label":"dcterms.creator","value":"Huang, Xiaowan"},{"label":"dcterms.dateAccepted","value":"2012-05-15T18:04:09Z"},{"label":"dcterms.dateSubmitted","value":"2012-05-15T18:04:09Z"},{"label":"dcterms.description","value":"Department of Computer Science"},{"label":"dcterms.format","value":"Application/PDF"},{"label":"dcterms.identifier","value":"http://hdl.handle.net/1951/55475"},{"label":"dcterms.issued","value":"2010-12-01"},{"label":"dcterms.language","value":"en_US"},{"label":"dcterms.provenance","value":"Made available in DSpace on 2012-05-15T18:04:09Z (GMT). No. of bitstreams: 1\nHuang_grad.sunysb_0771E_10395.pdf: 1116342 bytes, checksum: f193975afd47e801c71e2ae0912a87b1 (MD5)\n  Previous issue date:    1"},{"label":"dcterms.publisher","value":"The Graduate School, Stony Brook University: Stony Brook, NY."},{"label":"dcterms.subject","value":"Computer Science"},{"label":"dcterms.title","value":"Compiler-Assisted Software Model Checking and Monitoring"},{"label":"dcterms.type","value":"Dissertation"},{"label":"dc.type","value":"Dissertation"}],"description":"This manifest was generated dynamically","viewingDirection":"left-to-right","sequences":[{"@type":"sc:Sequence","canvases":[{"@id":"https://repo.library.stonybrook.edu/cantaloupe/iiif/2/canvas/page-1.json","@type":"sc:Canvas","label":"Page 1","height":1650,"width":1275,"images":[{"@type":"oa:Annotation","motivation":"sc:painting","resource":{"@id":"https://repo.library.stonybrook.edu/cantaloupe/iiif/2/57%2F82%2F39%2F57823948338967945041259212387802286634/full/full/0/default.jpg","@type":"dctypes:Image","format":"image/jpeg","height":1650,"width":1275,"service":{"@context":"http://iiif.io/api/image/2/context.json","@id":"https://repo.library.stonybrook.edu/cantaloupe/iiif/2/57%2F82%2F39%2F57823948338967945041259212387802286634","profile":"http://iiif.io/api/image/2/level2.json"}},"on":"https://repo.library.stonybrook.edu/cantaloupe/iiif/2/canvas/page-1.json"}]}]}]}