- Vardhan, Abhay. "Learning To Verify Systems," Ph.D. Thesis, Dept. of Computer Science, 2006. [pdf] [bib]
- Sen, Koushik, Abhay Vardhan, Gul Agha, Grigore Rosu. "Efficient Decentralized Monitoring of Safety in Distributed Systems," Submitted to Journal [invited], 2005. [pdf] [ps] [bib]
- Vardhan, Abhay, Mahesh Viswanathan. "Learning to Verify Branching Time Properties," Technical 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. [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]
Learning to Verify Systems
Making high quality and reliable software systems remains a difficult problem. One approach to address this problem is automated verification which attempts to demonstrate algorithmically that a software system meets its specification. However, verification of software systems is not easy: such systems are often modeled using abstractions of infinite structures such as unbounded integers, infinite memory for allocation, unbounded space for call stack, unrestricted queue sizes and so on. It can be shown that for most classes of such systems, the verification problem is actually undecidable (there exists no algorithm which will always give the correct answer for arbitrary inputs). In spite of this negative theoretical result, techniques have been developed which are successful on some practical examples although they are not guaranteed to always work. This dissertation is in a similar spirit and develops a new paradigm for automated verification of large or infinite state systems. We observe that even if the state space of a system is infinite, for practical examples, the set of reachable states (or other fixpoints needed for verification) is often expressible in a simple representation. Based on this observation, we propose an entirely new approach to verification: the idea is to use techniques from computational learning theory to identify the reachable states (or other fixpoints) and then verify the property of interest. To use learning techniques, we solve key problems of either getting positive and negative examples for the fixpoint of interest or of answering membership and equivalence queries for this fixpoint. We show that learning-based verification is a powerful approach: as long as one has suitable algorithms which can learn the fixpoints needed and decision procedures for some common set-theoretic operations, one can guarantee that the verification procedure will either find a bug or prove that the system is correct. In particular, we have seen that for a large number of practical systems, the class of regular languages is rich enough to express these fixpoints, allowing us to automatically verify such systems using learning algorithms for regular sets.
We show how the learning-based verification paradigm can be applied to a number of systems and for different kinds of specifications. First, we use learning to verify safety properties of finite state machines communicating over unbounded first-in-first-out channels. We assume that the reachable set of states is regular and use two different learning algorithms: one called RPNI which is based on learning from sample executions of the system, and the other derived from Angluin's L* algorithm which asks membership and equivalence queries. Next, we show how the learning approach can be used to verify safety properties of integer systems, parameterized systems and other systems in which states can be encoded as strings. We then extend the learning based approach to liveness properties and show how to use learning to verify omega-regular properties as well as CTL properties with fairness constraints.
We have implemented the above techniques in a tool called LEVER. We analyze various examples using the tool and show how LEVER successfully verifies their properties. The running time is also comparable to other tools available. Moreover, since we can prove that our method will terminate whenever the target set that we are computing is regular, this is a substantial improvement over other tools which can guarantee completeness only under very specific conditions. We also present a detailed case study of a module in the Linux kernel called read-copy-update mechanism and successfully verify some interesting properties using our learning based method.