Abstract: All aspects of our lives are becoming ever more complex. This is primarily due to our ever increasing expectations to live a life that is more comfortable, efficient, inclusive, etc. To achieve the expectations, we develop variety of complex systems, e.g. governments, corporations, hardware, software, etc. The expectations look deceptively simple. However, they are often in odds with each other and the sets of behaviors they expect from the systems are mathematically ugly and not analyzable using classical methods that have worked in basic sciences. We know from our personal experience that the systems are full of undesired behavior. Software are instances of such complex systems. An area of study has emerged, called formal verification, to develop theory and methods for ensuring reliability of software.
In this talk, we will discuss the principles involved in the area of formal verification. We will also see an introduction to the methods being developed to verify real world systems, e.g., airplanes, medical devices, facebook, windows, etc. Subsequently, we will see my current work in verification of concurrent programs under weak memory models. One will find that the ideas used in formal verification are also relevant in analysis of any other complex system.
