Abstract: 

The size and complexity of software, the labor cost of programming, and the dire consequences of software malfunction 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 verify software for safety and security. 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 building a platform to apply mathematics to reason about large software.

Venue: 2017 ACSS Conference, Patna, India, March 2017.

Author: Suresh Kothari