Compiler-assisted software model checking and monitoring

In this dissertation we present a compiler-assisted execution-based software model checking method targeting all languages that are acceptable by the compiler. We treat the intermediate representation of the program under compilation as a language and interpret it using a customized virtual machine. Our model checkers are based on this intermediate representation level virtual machine and have full access to its states. We implemented two model checkers: a stateless Monte Carlo model checker GMC2 and a bounded concrete-symbolic model checker using the dynamic path reduction algorithm for reachability problems of linear C programs.;We also introduce the new technique of Software Monitoring with Controllable Overhead (SMCO). SMCO is formally grounded in control theory, in particular, the supervisory control of discrete event systems. Overhead is controlled by dynamically disabling event interrupts, but such interrupts are disabled for as short a time as possible so that the total number of events monitored, under the constraint of a user-supplied target overhead, is maximized.;We have implemented SMCO using a technique we call Compiler-Assisted Instrumentation (CAI). Benchmark shows that SMCO successfully controls overhead across a wide range of target-overhead levels. Moreover, its accuracy monotonically increases with the target overhead, and it can be configured to distribute monitoring overhead fairly across multiple instrumentation points.