I work primarily on logic programming and formal methods. The main theme of my work has been to

- Formulate analysis and verification problems as query evaluation or inference over logic programs;
- Develop novel inference techniques to expand the scope of analysis problems that can be posed as query evaluation;
- Develop evaluation techniques so that the complexity and efficiency of query-based formulation matches those of specialized algorithms for the same analysis.

Most work described below were parts of Ph.D. theses of my students. The following is a brief summary of the significant developments described in detail in our publications.

We are currently working on expanding the class of models handled by our formulation and on the formulation of equivalence checking over such models.

We developed a symbolic algorithm for verifying ad hoc network protocols for unknown network topologies [SRS10]. Ad hoc network protocols pose a unique verification problem called instance explosion because an ad hoc network, with a fixed number of nodes, can assume exponential number of topologies. We developed a symbolic verification technique to combat this problem [SRS09]. Furthermore, we developed a parameterized verification technique for verifying ad hoc network protocols with arbitrary number of nodes.

We have investigated two ways of tackling this problem. The most
recent approach is to use partial model checking techniques for
generating a sequence of formulae, and computing the limit of this
sequence. More precisely, consider a parameterized system with
*n* instances of process *P*. To verify if
*P ^{n}* satisfies formula

We constructed partial model checkers for CCS/modal mu-calculus [BR03, BR06], and the pi-calculus/pi-mu-calculus [YBR06], and used this approach for verifying parameterized families of complex systems--- Java Meta Locking protocol with the former, and the Handover Protocol with the latter.

Earlier, we had investigated the use of logic programming
transformations for deriving automated induction proofs for
verification of parameterized families [RR04]. The key idea here was
to use the *fold* transformation, which replaces a part of a
clause body by an appropriate clause head, to simulate the effect of
the induction step. To apply this strategy for verification proofs,
we extended the folding step to work over clauses containing
disjunction as well as negation
[RKRR04,
RKRR02].

We have also looked at the verification of *linear-time*
properties of recursive programs more directly [BKPR02]. In that work, we
separated infinite runs into finite-stack runs (where the program
stack remains finite, but without an *a priori* bound) and possibly
stack-divergent runs. We constructed a model checker to check for
satisfaction of LTL properties for finite-stack runs, separately from
the satisfaction of the properties for all runs.

We have also considered several problems in the analysis of access control policies. Role-Based Access Control (RBAC) is a popular model for stating access control policies. Administrative RBAC (ARBAC) models are used to express how administrators in organizations can change the RBAC policies of that organization. Changes made by different administrators, all following the same ARBAC policy, may interact with each other in unforeseen ways. We considered the problem of analyzing ARBAC policies to check if RBAC policies with specific attributes are reachable via changes allowed by the ARBAC policy. By reducing the propositional planning problem to the ARBAC policy analysis problem, we established that the analysis problem is PSPACE-complete [SYSR11], and shown the computational complexity of several subsets of ARBAC policies.

We also considered interesting classes of ARBAC policies for which we
could devise analysis algorithms that have high complexity on an
usually small parameter characterizing the hardness of the input
[SYRG07].
These algorithms
were implemented at a high level as logic programs. More recently, we
investigated *symbolic* techniques for analyzing parameterized
ARBAC policies, where roles and permissions have parameters. Since
the parameters may range over infinite types, the analysis problem is
undecidable in general. We developed a semi-decision procedure for
this problem, and implemented based on query evaluation over
tabled constraint logic programs
[SYGR11].

We have also considered the problem of combine constraint processing with tabled evaluation, primarily to handle a larger classes of verification and analysis problems. For instance, we combined the handling of clock constraints into tabled evaluation in order to construct model checkers for timed systems [PRR02, DRS00]; dis-equality constraints for constructing model checkers and symbolic bisimulation checkers for value-passing systems [SYGR11, SRS09, YRS04, SR03a, BMRRV01]. One central problem in combining constraints solving and tabled evaluation was that the traditional constraint solvers maintained a global constraint store. Newly discovered constraints are added to this store, and entailment and consistency checks are performed against this central store. This strategy is followed even when constraint solvers are specified at a higher level, e.g. using constraint handling rules. In tabled evaluation, we need to keep multiple constraint stores, local to each query and answer. We developed an efficient technique for storing constraints in local stores, and evaluating constraint handling rules over such stores [SR07], thereby combining the power of tabled evaluation and constraint solving.

C. R. Ramakrishnan Last modified: Thu Feb 7 18:29:25 EST 2013