Ram Chandra Bhushan, MNNIT Allahabad, A CCS and MCRL2 Case Study: A Safety-Critical System (Slides)

Abstract

In computer science, model checking is a technique for automatically verifying correctness properties of finite-state systems. This paper deals with a model of a safety critical system named as "A level-crossing control system". The specifications of the model are first specified as processes in the calculus of communicating systems (CCS). The requirements of the system is written in the form of properties or formula in modal calculus, which has been verified then with the help of Concurrency Workbench (CWB-NC) tool. The same model is again modelled into a modeling language, MCRL2 which enables concise descriptions of the system.Specifications in MCRL2 has been simulated, visualized and verified against the requirements of the system using Mu-Calculus. It is motivated by a temporal logic specification. We also show that the safety requirements of the crossing satisfies with the help of tools supported by MCRL2 which enables us to express the necessary causality within the language itself.

Priyanka Darke, TRDDC (presented by Shrawan Kumar, TRDDC), Use of abstraction in code verification

Abstract

Deepak D'Souza, IISc, Decision Tree Based Learning of Program Invariants (Slides)

Abstract

Decision Tree based learning gives us an efficient way in practice, for learning a predicate from positive and negative examples. We discuss how to extend and apply this technique for learning loop invariants for proving assertions in programs. This is largely the work in the paper titled "Learning invariants using decision trees and implication counterexamples", by Garg, Neider, Madhusudan, and Roth, in POPL 2016. We will also discuss extensions of this approach to other styles of program proofs.

Inzemamul Haque, IISc, Verification of a Separation Kernel (Slides)

Abstract

A separation kernel is a microkernel which partitions the hardware resources among the 'partitions'. It is similar to a hypervisor. In this talk I shall present the work which we are doing to verify a separation kernel. We are working on an open-source separation kernel named Muen which is based on the x86 platform and uses hardware support for virtualization. It is written in Ada. My talk will consist of three parts - brief introduction of a separation kernel, Muen separation kernel and our technique and approach to verify it.

Kamal Lodaya, IMSc, Between Two- and Three-Variable Logic on Word Models (Slides)

Abstract

On linear orders, Kamp (1969) proved that every sentence of first order logic can be defined using three variables, and he introduced binary modalities such as "until" in temporal logic to obtain expressive completeness. This followed an algebraic characterization by Schutzenberger (1965). First order logic with two variables, into which modal logic and temporal logic with unary modalities embed, is much weaker. Another of Schutzenberger's algebraic characterizations (1976) and later work by Therien and Wilke (1998) showed that it corresponds to Sigma2 intersection Pi2 in the quantifier alternation hierarchy of first order logic (Thomas, 1982). Recent results on levels of this hierarchy were obtained by Place and Zeitoun (2014). Motivated by the fact that "betweenness" is an obvious property inexpressible in two-variable logic, we introduced (with Krebs, Pandya and Straubing) two-variable logic with betweenness properties thrown in, and obtained some technical results (2016). In this talk we review this literature.

Kumar Madhukar, TRDDC, Counterexample-Guided Quantifier Instantiation for SMT (Slides)

Abstract

This talk will be based on a CAV 2015 paper with the same title. The authors present an approach that extracts solution functions from unsatisfiability proofs of the negated form of synthesis conjectures. The paper also discusses novel counterexample guided techniques for quantifier instantiation that are used to make finding such proofs practically feasible.

Madhavan Mukund, CMI, Distributed Games (Slides)

Abstract

Realizability, or synthesis, is the problem of automatically constructing a reactive system from a functional specification of its input-output behaviour. A closely connected problem is controllability, which asks for a control strategy to restrict the behaviour of an open system to meet a behavioural specification. Both problems have a natural connection to games. The Büchi-Landweber theorem (1969) provides a solution to the realizability problem in the sequential setting. Pnueli-Rosner (1989) showed that the same problem is undecidable in a distributed setting where the architecture is part of the specification. Gastin-Lehrman-Zeitoun (2004) proposed an alternative model for distributed games, based on Mazurkiewicz trace theory, with local strategies based on causal memory, and showed decidability for series-parallel dependency alphabets. Decidability of this model remains open in the general case.

Paritosh Pandya, TIFR, Formalizing Timing Diagram Requirements in QDDC

Abstract

Several temporal logics have been proposed to formalise timing diagram requirements over hardware and embedded controllers. These include LTL [CF05], discrete time MTL [AH93] and the recent industry standard PSL [EF16]. However, succintness and visual structure of a timing diagram are not adequately captured by their formulae [CF05]. Interval temporal logic QDDC is a highly succint and visual notation for specifying patterns of behaviours [Pan00]. In this paper, we propose a practically useful notation called SeCeNL which enhances negation free fragment of QDDC with features of nominals and limited liveness. We show that timing diagrams can be naturally, compositionally, and succintly formalized in SeCeNL as compared with PSL-Sugar and MTL. We give a linear time translation from timing diagrams to SeCeNL. As our second main result, we propose a linear time translation of SeCeNL into QDDC. This allows QDDC tools such as DCVALID [Pan00,Pan01] and DCSynth to be used for checking consistency of timing diagram requirements as well as for automatic synthesis of property monitors and controllers. Giving a theoretical analysis, we show that SeCeNL satisfiability and model checking have elementary complexity as compared to the non-elementary complexity for the full logic QDDC. (joint work with Rajmohan Matteplackel (TIFR) and Amol Wakankar (BARC)).

Souradyuti Paul, IIT GN, Smart Contracts and Formal Methods

Abstract

Abhisekh Sankaran, IMSc, A Finitary Analogue of the Downward Lowenheim-Skolem Property (Slides)

Abstract

We present a model-theoretic property of finite structures, that can be seen to be a finitary analogue of the well-studied downward Löwenheim-Skolem property from classical model theory. We call this property the equivalent bounded substructure property, denoted EBSP. Intuitively, EBSP states that a large finite structure contains a small ``logically similar'' substructure, where logical similarity means indistinguishability with respect to sentences of FO/ MSO having a given quantifier nesting depth. It turns out that this simply stated property is enjoyed by a variety of classes of interest in computer science: examples include regular languages of words, trees (unordered, ordered, ranked or partially ranked) and nested words, and various classes of graphs, such as cographs, graph classes of bounded tree-depth, those of bounded shrub-depth and m-partite cographs. Further, EBSP remains preserved in the classes generated from the above using various well-studied operations, such as complementation, transpose, the line-graph operation, disjoint union, join, and various products including the Cartesian and tensor products. All of the aforementioned classes admit natural tree representations for their structures. We use this fact to show that the small and logically similar substructure of a large structure in any of these classes, can be computed in time linear in the size of the tree representation of the structure, giving linear time fixed parameter tractable (f.p.t.) algorithms for checking FO/MSO definable properties of the large structure. We conclude by presenting a strengthening of EBSP, that asserts "logical self-similarity at all scales" for a suitable notion of scale. We call this the logical fractal property and show that most of the classes mentioned above are indeed, logical fractals.

S P Suresh, CMI, Consensus Algorithms and Blockchain (Slides)

Abstract

Bitcoin, Ethereum and the blockchain technology that drives them have received a lot of attention in the recent past from technologists, businessmen, economists and computer scientists. This talk provides a gentle introduction to blockchain with special emphasis on the solution to the consensus problem that forms the backbone of blockchain. The talk is intended to expose the formal methods community to the ideas used in blockchain and interest them in working on the theoretical underpinnings.

S P Suresh, CMI, Knowledge transfer and information leakage in protocols (Slides)

Abstract

Traditionally, information flow in protocols has been analyzed using notions of entropy. We move to a discrete approach where information is measured in terms of propositional facts. We consider protocols involving agents holding numbered cards who exchange information to discover each others' private hands. We define a transition system that searches the space of all possible announcement sequences made by such a set of agents and tries to identify a subset of announcements that constitutes an informative yet safe protocol.