Interprocedural Analysis and the Verification of Concurrent Programs

Опубликовано 6 сентября 2016, 18:50

In the modern world, not only is software getting larger and more complex, it is also becoming pervasive in our daily lives. On the one hand, the advent of multi-core processors is pushing software towards becoming more concurrent. On the other hand, software is everywhere, inside nuclear reactors, space shuttles, cars, traffic signals, cell phones, etc. In meeting this demand for software, reliability will be a key factor, for which program verification plays an important role. My research addresses both of these challenges. First, I designed new techniques for the verification of concurrent programs. My thesis explores the problem of context-bounded verification, where only those concurrent behaviors that have a bounded number of context switches between threads are considered. We show that context-bounded verification provides a viable alternative to full verification because it can be very efficient and most bugs can be found in a few context switches. Second, along with colleagues at Wisconsin, I designed a model checker for machine code. In many scenarios, including those with malicious software, source code or debugging information may not be available. In those cases, it is necessary to have a tool that can understand machine code. My thesis shows how we went about systematically building an infrastructure for machine code for use inside a verification tool called McDash. We give evidence that McDash can understand the intricacies of low-level code, while competing well with source-level tools.