The size and complexity of software, the labor cost of programming, and the dire consequences of software malfunctioning have made it a nightmare to maintain software-intensive cyber-physical systems. Agile development, programming languages, component libraries etc. help but they do not suffice to ensure correctness and cost-effective maintenance of complex software. The central question is: how do we systematically reason about large software?
This talk will trace the history of a branch of mathematics and how that mathematics is likely to be the key to advance software engineering and its application to ensure safety and security of cyber-physical systems. While mathematics is crucial, being able to apply it to real-world software with millions of lines of code poses a colossal engineering challenge. The talk will present examples of sophisticated malware and a software verification study of the Linux kernel to illustrate our research on advancing the mathematics and building a platform to apply the mathematics to reason about large software.
Author: Suresh Kothari