Research Interests

I have generally been interested in Computer Science in its entirety.
However, I have a special affection towards theoretical aspects, in particular in the applications of Logic and Automata theory in formal verification of programs and cyber-physical systems.
I have also started getting interested in concurrency,program synthesis, theorem proving, programming languages and distributed systems

Projects

Ongoing Work

Proof Search for Program Synthesis : Given a high-level specification, can we automatically generate programs that meet the specification ? Program synthesis is an active area of research that aims to find answers to this question. In the past few years, inductive program synthesis has gained a lot of attention. We propose that program synthesis can be made efficient, if we search for proofs for correctness of programs, and derive programs from such proofs. We show that such a technique reduces the complexity of compnent-based program synthesis from an problem to an problem. We show the utility of the technique by synthesizing security protocols and cryptographic schemes.

Verification of Linear Hybrid Systems : We propose a class of Linear Hybrid Systems, called aligned hybrid systems. We show that reachability analysis of these models is efficiently decidable. We then show how arbitrary linear hybrid models can be abstracted to an aligned model, and then perform counter-example guided abstraction refinement to check for reachability in arbitrary systems.

Dynamic Race Detection in Linear Time : Writing reliable concurrent software still remains a huge challenge for programmers. This is because it is difficult to reason about all possible interleavings of a concurrent program, which becomes tremendous for large scale software. This calls for the need for automatic tools to check for (potential) races. Since, checking for races by statically analyzing the code is undecidable in general. Most techniques that employ static analysis techniques are typically unsound and raise a lot of false alarms. Typically, dynamic race detection tools rely on Lamport's happens before relation for checking races. These techniques construct some partial orders from a given execution trace and check if there are two conflicting events that are unordered by this relation. While happens before is a sound characterization, it fails to detect many races. Recent works on extending this relation (see causally precedes ) run in time that is polynomial in the size of the traces. Other models like RV-Predict's maximal sound predictive algorithm also run in time that is not linear. These techniques do not scale really well when execution traces become large, and typically address this issue by windowing on the traces, which can potentially lead to imprecision in their race detection capabilities. In this work, we have devised a sound characterization for race detection, that is a generalization of the causally-precedes relation, and can be implemented in linear time. Email me if you wish to test the tool that I developed.

Conformance testing for Linear Dynamical Systems : We consider dynamical systems for which the rate of evaluation of the continous parameters is given as a set of linear differential equations. Such systems can be ued to model many embedded / interactive systems. Examples include automated thermostats. We consider the problem of testing conformance of two linear dynamical systems. Two systems are conformant if their dynamic behavior is similar. This means that for every execution in one of the systems, there is a similar execution in the other system. This problem is often encountered in analysis of systems from the perspective of verification.

Verification of Probabilistic Recursive Programs : Analysis of probabilistic programs is central to many areas such as cryptography and security. While there are available tools that perform analysis of probabilistic systems (see PRISM for example), the subjects of analysis are typically finite state models, and do not focus on programs (say with recursion). We address this problem and have devloped a tool for the analysis of probabilistic recursive programs. We modelled probabilistic recursive programs as probabilistic pushdown systems, by representing program statements as transition rules of the PDS and the relations on the variables symbolically as MTBDDs (Multi Terminal BDDs). We used fixed point iteration methods to compute the probabilities attained by different valuations on program variables at different program points. and integrated the tool with an already exisitng BDD-based framework (Moped). The tool also provides quantitative and qualitative analysis for temporal properties. We also computed metrics like min-entropy to determine the amount of information leakage from the program.
Poster | Proped Slides

Past Projects

Modelling Hybrid Systems using Weak Singular Hybrid Automata : While Hybrid Automata provide very expressive and generic framework for modelling cyber-physical systems, most interesting questions like reachability and temporal model-checking remain undecidable for it. We propose a new subclass of Hybrid Automata called Weak Singular Hybrid Automata (WSHA) which are so-far the most expressive subclass for which reachability, schedulability and LTL model checking are decidable even in absence of any known finite bisimulation. We showed that reachability and schedulability are NP-complete and LTL-model checking is PSPACE complete for this model. We also showed that CTL-model checking on this model is atleast PSPACE-hard. We further propose that the model lies on the frontiers of decidability boundaries by showing that the reachability problems for natural extensions to the proposed model become undecidable.
Slides

Computing Information Flow Using Symbolic Model Checking : Several measures have been proposed in literature for quantifying the information leaked by the public outputs of a program with secret inputs. We consider the problem of computing information leaked by a deterministic or probabilistic program . The key challenge in computing these measures is that we need the total number of possible outputs and, for each possible output, the number of inputs that lead to it. A direct computation of these quantities is infeasible because of the state-explosion problem. We therefore propose symbolic algorithms based on binary decision diagrams (BDDs). The advantage of our approach is that these symbolic algorithms can be easily implemented in any BDD-based model-checking tool that checks for reachability in deterministic non-recursive programs by computing program summaries. We demonstrate the validity of our approach by implementing these algorithms in a tool called Moped-QLeak, which is built upon Moped, a model checker for Boolean programs. Finally, we show how this symbolic approach extends to probabilistic programs.
FSTTCS Slides | MVD Slides

Non-Zeno strategies for Timed Games : Games on Hybrid systems can be used to efficiently model controllers for cyber-physical systems. We considered 2-player concurrent games on timed automata with the objective of characterizing conditions under which a scheduler can avoid Zeno runs. We devised sound and complete requirements for the region-abstract model of such a system to have a non-Zeno strategy, by transforming the untimed abstract game into a Büchi game setting. We also proposed a method to concretize the abstract strategy to derive a concrete strategy for a scheduler.
Slides