Evolution-aware runtime verification

The risk posed by software bugs has increased tremendously as software is now essential to many aspects of our daily lives. Software testing is still the most common method for finding bugs during software development, before software is deployed. However, software testing alone is insufficient for finding bugs, as evidenced by the many devastating bugs that frequently manifest in deployed software. Hence, there is a great need to investigate how to use formal-methods based approaches effectively and efficiently during software testing, to help find more bugs during software development. This dissertation presents work on finding more bugs during software development by performing runtime verification during software testing. Runtime verification can help find bugs by monitoring program executions against formally specified properties. Over the last two decades, great research progress has improved the performance of runtime verification, but mostly focused on deployed software. There was little focus on the bug-finding benefits and scalability challenges of using runtime verification during testing of evolving software. Yet, software testing generates many executions on which properties can be monitored to squeeze more bug-finding value from existing tests. This dissertation presents two lines of work on studying and improving the use of runtime verification for finding more bugs during testing of evolving software. Firstly, this dissertation reports on the first large-scale study of runtime verification during software testing. The study performs runtime verification using 199 properties while running 18K developer written tests and 2.1M automatically generated tests in 200 open-source projects. Results show that runtime verification during software testing finds many bugs from existing tests, but incurs high overhead. In spite of tremendous recent research and algorithmic advances in the runtime verification community on improving the runtime overhead, user experience, and monitored properties, runtime overhead was still as high as 33.9x, many property violations were generated that had to be manually inspected, and 84% of the inspected violations were not bugs due to the ineffectiveness of current properties. Secondly, this dissertation proposes the idea of, and implements the first set of techniques for, reducing the overhead of runtime verification during software testing by exploiting software evolution. All prior runtime verification research focused on checking a single version of software. The proposed evolution-aware techniques extend runtime verification to support multiple software versions and make runtime verification more usable during software evolution. The key insight behind the evolution-aware techniques is to amortize the overhead of runtime verification across multiple versions by only monitoring the parts of code that changed between versions. Results show that evolution-aware techniques reduce the accumulated runtime verification overhead by up to 10x and show developers two orders of magnitude fewer violations, without missing new violations. We expect the benefits of evolution-aware runtime verification to still apply after future research yields more effective properties with higher rates of bugs found per violation