I finished my PhD at the Univeristy of Illinois in Fall 2005. I am now working in Google in California.

I am broadly interested in techniques and methods to help with verification of software systems. More specifically, I am working on applying techniques from machine learning and language inference for verification. For most infinite state sytems a naive model checking approach cannot be used because it tries to exhaustively explore the entire state space. The central idea in my approach is to try to learn the fixpoints needed for verification instead of computing them iteratively. This way we have the hope of learning the correct set even if it is infinite. The interesting result is that if the system that we are analyzing does have a set representable in the class we learn, then we have a sound as well as a complete method for verification. I have developed a paradigm for "learning to verify" and instantiated this for FIFO automata, parameterized systems, systems with unbounded integers (see publications) and other models which use regular sets to represent sets of states. We can analyze safety as well as liveness (omega-regular and CTL) properties with this method. The abstract for my dissertation can be found here.

An 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 and techniques for refining specifications into actual implementation.

Select publications

Sen, Koushik, Abhay Vardhan, Gul Agha, Grigore Rosu. "Efficient Decentralized Monitoring of Safety in Distributed Systems," Submitted to ACM TOSEM [invited], 2006. [pdf] [ps] [bib]
Vardhan, Abhay. "Learning To Verify Systems," Ph.D. Thesis, Dept. of Computer Science, 2006. [pdf] [bib]
Vardhan, Abhay, Mahesh Viswanathan. "Learning to Verify Branching Time Properties," Techincal Report UIUCDCS-R-2004-2445, UILU-ENG-2004-1747 (this is a long version of a paper to appear at the 20th IEEE/ACM International Conference on Automated Software Engineering, Long Beach, California, USA), 2005. [pdf] [bib]
Vardhan, Abhay, Koushik Sen, Mahesh Viswanathan, Gul Agha. "Using Language Inference to Verify omega-regular Properties," In Proceedings of 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005), LNCS, 2005. [pdf] [ps] [bib]
Vardhan, Abhay, Koushik Sen, Mahesh Viswanathan, Gul Agha. "Actively Learning to Verify Safety for FIFO Automata," In 24th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'04), Lecture Notes in Computer Science, Chennai, India, December, LNCS 3328, pages 494-505, Copyright Springer-Verlag (http://www.springer.de/comp/lncs/index.html), 2004. [pdf] [ps] [bib]
Sen, Koushik, Abhay Vardhan, Gul Agha, Grigore Rosu. "Efficient Decentralized Monitoring of Safety in Distributed Systems," In Proceedings of 26th International Conference on Software Engineering (ICSE'04), pages 418-427, Edinburgh, UK, May 2004. IEEE., 2004. [pdf] [ps] [bib]
Vardhan, Abhay, Koushik Sen, Mahesh Viswanathan, Gul Agha. "Learning to Verify Safety Properties," In 6th International Conference on Formal Engineering Methods (ICFEM'04), Seattle, WA, USA, November 2004, LNCS 3308, pages 274-288, Copyright Springer-Verlag (http://www.springer.de/comp/lncs/index.html), 2004. [pdf] [ps] [bib]
Sen, Koushik, Abhay Vardhan, Gul Agha, Grigore Rosu. "On Specifying and Monitoring Epistemic Properties of Distributed Systems," In 2nd International Workshop on Dynamic Analysis (WODA'04), Satellite workshop of ICSE 2004, pages 32-35. British Institution of Electrical Engineers (IEE), May 2004., 2004. [pdf] [ps] [bib]
Vardhan, Abhay, Gul Agha. "Using Passive Garbage Collection Algorithms for Garbage Collection of Active Objects," International Symposium for Memory Management, pp 106-113, Berlin, June 20-21, 2002. [pdf] [ps] [bib]
Vardhan, Abhay, P. L. Dhar. "A new procedure for performance prediction of air conditioning coils," International Journal of Refrigeration , Volume:21, Issue: 1, pp. 77-83, 1998. [bib]
Vardhan, Abhay. "Distributed Garbage Collection of Active Objects: A Transformation and its Applications to Java Programming," MS Thesis, University of Illinois, 1998. [pdf] [bib]
Rao, J. S., V. P. Agrawal, Abhay Vardhan, Lakhbir S. Lamba. "Computer Aided Learning of Planar Linkages," Proceedings of the Ninth World Conference on the Theory of Machines and Mechanisms, Milan, Italy, p 3176-80, 1995. [bib]