Abstract: Software malfunctions can have catastrophic consequences and enormous costs. The error-prone and laborious manual practices of developing and maintaining large software must change to cope with ever increasing complexity of software, and the enormous safety and security challenges it poses. Formal verification is not a practical alternative for large software; it is riddled with problems of low accuracy and high computational complexity. The need for automation in software engineering is undoubted, however, a human is indispensable to reason about complex software. With this background, we have conducted two decades of research on human-in-loop automation (HLA) as a pragmatic alternative to manage complexity, safety, and security of large software systems in the cyber-physical world.

This course will introduce the HLA technology developed through our research, with unprecedented capabilities to model, analyze, visualize, verify, and transform large software in multiple languages. The HLA technology incorporates a graph database platform with a powerful query language to extract knowledge from software and build visual models to solve complex problems through automation guided by human reasoning. The HLA technology has been validated by applying it to: automatic parallelization of climate model software, model-based software development for critical avionics and automobile control systems, safety verifications of the Linux operating system, and cybersecurity challenges posed by Defense Advanced Research Projects Agency (DARPA) research programs. More than 300 companies including all major avionics and automobile companies use the HLA tools developed by EnSoft, the company founded on our research.

This course will provide a solid foundation on fundamentals of software that are applicable across all programming languages. With examples of real-world software problems, we will elaborate how this fundamental knowledge can be applied using HLA to cope with software complexity, safety, and security. We will present HLA as a modeling and problem-solving activity. Starting with a HLA model for systematic debugging, the course will show how to gradually advance to build HLA models for verifying complex software such as the Linux kernel. As in physics and mathematics, rigorous problem solving will be taught with models as powerful abstractions. We will use the Atlas platform from EnSoft to build visual models of software. Atlas stores program semantics in a graph database, and provides interactive and programming interfaces to query, model, and visualize software.

A strong laboratory component will include demonstrations, interactive experiments, and programming exercises. The labs will include challenging problems from real-world software in C, Java, and Java byte code. The participants will get a first-hand experience of how to implement HLA techniques through Atlas and perform analysis tasks in few minutes. These will include examples of difficult analysis tasks for which automated analysis is intractable, manual effort is prohibitively high, and thus HLA is the only practical solution.

The lecture notes, exercises, and the HLA tools for conducting the labs will be available to the participants for free academic use. The course will provide transformative ideas and introduce tools to implement them. It will enable academic participants to transform their research and education to focus on real-world problems of large software. It will impel new thinking among industry and government participants to innovate application-specific HLA practices and tools that can save significant time, money and effort with unprecedented capabilities to achieve safety and security in their software systems.

Venue: Global Initiative of Academic Networks (GIAN), Malaviya National Institute of Technology, Jaipur, India, September 12-16, 2016.

Instructors: Suresh Kothari, Benjamin Holland

Materials: https://github.com/benjholla/GIAN2016

GIAN Short Course in Jaipur, India 2016