Abhay Vardhan

Photo

Email: vardhan_AT_uiuc.edu

Education

Research


Software programs are often buggy. This is painfully obvious in almost all computer systems that we use daily; with almost predictable frequency, security holes are discovered, programs do not behave as expected and operating systems crash. Some well-known disasters such as Ariane 5 explosion, Patriot-Scud failure, loss of Mars Climate Orbiter and Pentium division bug, have all been attributed to very simple programming errors (see Collection of Software Bugs). A NIST study in 2002 estimated that software errors cost $59.5 billion annually in the United States alone.

Traditionally, the most common method of finding bugs has been testing. However, it is recognized that as systems get more and more complex, exhaustively testing all possible scenarios is impossible. This is even more true of concurrent systems where bugs may be revealed only under some uncommon scenarios. In the last few years, "automated verification" techniques have emerged as a powerful alternative to find bugs which are difficult to catch using other means. However, in the context of verification of software systems, this is hard since such systems typically have very large or even infinite state space.

I have developed a new paradigm for verification of infinite or large state-space systems. Our idea relies on the following insight. We know that verification of systems usually entails computing either the set of states reachable from the initial states or certain fixpoints associated with logical formulas. For many practical systems, even though the set of reachable states (or the fixpoints) is infinite, it is often highly structured and is expressible in a simple representation, for example as a regular sets. There is a rich body of work referred to as computational learning theory which, among other things, deals with learning concepts such as regular sets and other languages. If we can provide the information needed to learn the reachable states or the fixpoints, then we can hope to compute these directly and thus solve the verification problem. This is the main question I have addressed in my work. Our central thesis is that techniques from computational learning theory can indeed be used effectively for verifying different classes of infinite state systems and various kinds of properties. I have demonstrated that this is an attractive technique for analyzing practical systems. We show how to solve the key problems needed for using learning techniques: either getting positive and negative examples of the fixpoint of interest or answering membership and equivalence queries for this fixpoint. To our knowledge, this is the first systematic attempt to view verification as a learning problem, although some ideas from learning have been used in the past for verification.

The "learning to verify" paradigm has been used succesfully for FIFO automata, parameterized systems, systems with unbounded integers (see publications) and other models which use regular sets to represent sets of states. Safety as well as liveness (omega-regular and CTL) properties can be analyzed with this method and an implementation is available in a tool called LEVER (available for download). The abstract for my dissertation can be found here.

Another important light weight method to identify bugs in software systems is to use monitoring techniques at run time to check if the specification is violated. I have worked on techniques for efficiently monitoring safety properties for distributed systems.

I am also interested in specification languages, techniques for refining specifications into actual implementation, model driven development and security in software systemms.
Other work that I have done in the past:
To research group's main page

Select publications

Tools

Work

Other interesting links to University of Illinois
Other Interesting Places to go to
Last modified: Tue Nov 15 19:47:59 CST 2005