Research Statement Multi-valued Model-checking

As computers get faster and smaller, they are becoming more pervasive in our daily lives. At the same time, software systems that control them are becoming larger, more complex, and error prone. Software bugs lead to a loss of productivity, denial of service, and security breaches, cost millions of dollars to the economy, and sometimes cause a loss of human life. I believe that formal methods are indispensable for building reliable and trusted software systems of the future. However, formal methods are not yet widely used in industry outside of the safety-critical and hardware domains. An often cited reason is that they are perceived to require a level of mathematical sophistication beyond that possessed by many software developers. I believe that the key to addressing this problem is in constructing automated reasoning techniques and developing methodologies to support their use by software developers. The dream of a “mechanical verifier” has been pursued by the research community since the 60s. However, only recently the success of such projects as Microsoft’s Static Driver Verifier (SLAM) and the increased success of formal verification in hardware industry has clearly demonstrated that this dream is becoming a reality. The main goal of my research is to facilitate the construction of reliable and trusted computer systems by developing tools and methodologies to improve usability and to extend the scope of application of formal methods in software engineering. I believe that the success in this area crucially depends on the combination of foundational, engineering and software engineering approaches. A strong theoretical foundation is necessary to understand and solve any problem. Building such a foundation requires developing new theories and discovering novel combinations of existing ones. At the same time, turning a theory into an automated analysis tool is often a significant engineering effort. Finally, an automated analysis tool is only effective when combined with a solid software engineering methodology that enables its use by practicing software engineers. In my research, I aim to combine the three approaches by starting from a real-life problem, developing a theoretical solution, engineering systems based on this solution, and finally conducting case studies to study the effectiveness of the approach.