Developing a decentralized configuration management system for a distributed cloud storage system by integrating blockchain and software defined storage is addressed in this talk. The system should be capable of generating, distributing, and applying configuration files among nodes in a storage network in a stable, and decentralized manner. By achieving this, the software defined storage gains the decentralized management capability, while still benefiting from its established capabilities in guaranteeing storage service quality. To ensure the system's effectiveness and prevent unforeseen problems, a formal model of the decentralized configuration management system was created and evaluated using model-checking. At the end, we discuss our experience of deploying the primitive Durna system.

We consider the following question.

Given a global transition system TS over a set of actions A, together with a distribution of A into local components (A_1,...,A_k), does there exist a distributed transition system over (A_1,...,A_k) that is "behaviourally equivalent" to TS?

We focus on two variants of distributed transition systems --- loosely cooperating systems and synchronously communicating systems. For behavioural equivalence, natural choices are language equality and bisimulation.

For some combinations of system model and behavioural equivalence, the problem has been solved decades back. Somewhat surprisingly, other versions of the problem still remain open. We will survey the state of the art.

A multi-agent Kripke structure can model beliefs of agents. Baltag, Moss and Solecki (1998) introduced action frames to describe views by different agents of a single action. Updating a Kripke structure by an action frame models belief change.

Beliefs can be false. Lying actions are those which induce false beliefs. In our work we also allow deceptive actions which induce fictitious agents. These ideas were applied to an AI planning problem of modelling a story.

Multi-agent modal logic can be used to describe Kripke structures and hence sets of beliefs. In this talk we consider the model checking problem for a suitable modal logic (dynamic epistemic logic) and its complexity.

This is joint work with Shikha Singh (i3 Digital Health) and Deepak Khemani (Plaksha).

SMT can automate reasoning about decidable logical fragments, but are rather unpredictable when it comes to reasoning about arbitrary user-defined functions. We describe a new approach to automating the verification of properties of such functions. First, we show how to reflect the code implementing such user-defined functions into the function's output type (i.e. post-condition), thereby ensuring that each invocation, the function definition is precisely instantiated in a manner that permits decidable verification.

Second, we show how reflection exploits the propositions-a-types principle, to let the user write equational proofs of programs just by writing other programs e.g. using pattern-matching and recursion to perform case-splitting and induction. Finally, we introduce a proof-search algorithm called Proof by Logical Evaluation that uses techniques from model checking and abstract interpretation, to completely automate equational reasoning about functions using SMT.

In 1984, Tony Hoare articulated the paradigm "Programs are Predicates". Following this, we give a specification oriented semantics of Concurrent, real-time programs using a versatile temporal logic -- Duration Calculus (DC). Each operator of the programming language is modelled as a derived logical connective of DC. Specific assumptions about the nature of concurrency and time can be modularly plugged in as axioms giving a variety of models including the "Maxpar" model. The resulting formulation serves simultaneously as a compositional semantics as well as an axiomatic proof system.

Real-time Operating Systems (RTOSs) are widely used to design and develop embedded safety critical software applications. Such applications have to be fault tolerant, deterministic and meet stringent safety standards which include several functionality-related real-time requirements. The applications rely on, and use several features of the underlying RTOS to satisfy these design requirements. Real-time operating systems provide kernel APIs and scheduling algorithms to cater to many of the safety requirements. We will discuss our experience of formally verifying several safety critical requirements of one such indigenous RTOS that has time and space partitioning features and is being used by the Indian avionics industry.

First order logics and propositional modal logics have been studied extensively in computer science, for their model theoretic and algorithmic properties. The situation with first order modal logics (FOML) is discouraging, with even extremely weak fragments (such as unary predicates) being undecidable. However, work in the last decade has managed to find new ways of combining quantifiers and modalities to find decidable fragments, leading to a range of open questions. In this talk, we give an outline of these developments.

Abstracting from earlier work on a dynamic (heterogeneous) core allocation and management scheme for H.264 video decoding that reduces energy costs while delivering desired frame rates, we formulate operationally the general problem of executing a sequence of actions on a reconfigurable machine while meeting a corresponding sequence of absolute deadlines, with the objective of reducing cost.

Using a transition system framework that associates costs (e.g., time, energy) with executing an action on a particular resource configuration, we formulate a very simple by general version of simulation relations for cumulative cost transition systems. This notion of simulation forms the basis for specifying deadline/budget-conformant executions, and appropriate notions for comparing such executions. These simulation-based notions can provide the basis for an operational theory of optimal cost executions and performance guarantees for approximate solutions, in particular relating the notion of simulation from transition systems to that of competitive analysis used for, e.g., online algorithms.

Many know of Professor S. Arun-Kumar (SAK) as a concurrency theorist. What is less well known is that he is also a hacker, having spent a year building a front-end for the Concurrency Workbench automatic verification tool using the Process Algebra Compiler (PAC)! I will reflect on this experience, and other (all too few) times that our careers have overlapped. I will also talk about recent results of mine and a colleague’s on fixpoint logics for timed automata, a model of computation that SAK and his collaborators have also devoted significant attention to.