Research | Research |
|
In my Ph.D. work, I developed a new paradigm for verification of infinite or large state-space systems using techniques from computational learning theory. I showed that oracles can be constructed for answering membership and equivalence queries which can then be used by to learn certain fixpoints allowing various verification questions to be answered. The learning based verification method enjoys several nice properties. First, the running time of the verification algorithm depends not on the time taken to converge to the fixpoint (which may not even be achievable in a finite number of steps) but on the size of the symbolic representation of the fixpoint. Second, it avoids the space overhead of computing intermediate approximations to the fixpoint. Finally, the learning based verification method is sound (it never gives an incorrect answer) and if the fixpoint set is representable in the symbolic representation used by the learner, it is also complete (it is guaranteed to terminate). The "learning to verify" paradigm has been used successfully 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). Thesis abstract and PDF. 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 systems. Other work that I have done in the past:
Related: Comparision shopping |
| < Prev |
|---|