C Aiswarya, Chennai Mathematical Institute, Reachability in Database-driven Systems with Numerical Attributes under Recency Bounding

Abstract

A prominent research direction of the database theory community is to develop techniques for verification of database-driven systems operating over relational and numerical data. Along this line, we lift the framework of database manipulating systems which handle relational data to also accommodate numerical data and the natural order on them. We study an under-approximation called recency bounding under which the most basic verification problem — reachability, is decidable. Even under this under-approximation the reachability space is infinite in multiple dimensions – owing to the unbounded sizes of the active domain, the unbounded numerical domain it has access to, and the unbounded length of the executions. We show that, nevertheless, reachability is ExpTime complete. Going beyond reachability to LTL model checking renders verification undecidable.
Joint work with Parosh Aziz Abdullah, Mohamed Faouzi Atig and Marco Montali (PODS 2019).

Muqsit Azeem, TRDDC Pune, Learning Linear Temporal Properties

Abstract

We present two novel algorithms for learning formulas in Linear Temporal Logic (LTL) from examples. The first learning algorithm reduces the learning task to a series of satisfiability problems in propositional Boolean logic and produces a smallest LTL formula (in terms of the number of subformulas) that is consistent with the given data. Our second learning algorithm, on the other hand, combines the SAT-based learning algorithm with classical algorithms for learning decision trees. The result is a learning algorithm that scales to real-world scenarios with hundreds of examples, but can no longer guarantee to produce minimal consistent LTL formulas. We compare both learning algorithms and demonstrate their performance on a wide range of synthetic benchmarks. Additionally, we illustrate their usefulness on the task of understanding executions of a leader election protocol.

Purandar Bhaduri, IIT Guwahati, Admissible Strategies for Safety and Reachability Objectives in Graph Games

Abstract

Finding winning strategies for Player 1 (the system) against Player 2 (the environment) in graph games is the basis for synthesizing controllers satisfying a specification. In many situations where winning strategies do not exist, it is important to compute admissible strategies -- strategies that are not dominated by any other Player 1 strategies. In this work, we address the problem of computing admissible strategies for safety and reachability objectives in graph games. The problems are in PSPACE. Our algorithms are graph-theoretic in nature and have exponential time complexity.

Sayan Mukherjee, Chennai Mathematical Institute, Timed Automata and Diagonal Constraints

Abstract

This talk is about the reachability problem in timed automata. In particular, we will look at what are 'diagonal constraints' in timed automata transitions and what are the advantages of using them. We will go over the popular algorithm using ‘zones’ for checking reachability in timed automata without diagonal constraints. We will describe the difficulties in extending this algorithm to the case of diagonal constraints and show how we can potentially circumvent this difficulty.

Madhavan Mukund, Chennai Mathematical Institute, Model Learning

Abstract

The goal of model learning is to build transition systems for software and hardware systems through experiments, where one provides inputs and observes outputs. We survey some algorithms proposed in the black-box setting, where no information is available a priori about the internal structure of the system. The design of algorithms for model learning constitutes a fundamental research problem.

N V Narendra Kumar, IDRBT, Formalizing Secure Information Flow

Abstract

Information flow security is a general notion of security that encompasses many specific security properties desired in practice. In this talk, we will look at some of the important developments in the literature to formalize the notion of information flow security. In particular, we will discuss Fenton’s “Data Mark Machine”, Denning’s “Lattice Model” and “Certification Semantics”, various notions of “Non-interference” including that of Goguen & Meseguer, and Volpano, Smith & Irvine, Myers & Liskov’s “Decentralized Information Flow Control” and the related notions of “Declassification” and “Endorsement”. We will conclude with a discussion on the “Readers-Writers Flow Model” developed by Naren & Shyamasundar.

Ramchandra Phawade, IIT Dharwad, Timed Context Sensitive Languages

Abstract

TBA

Sumanth Prabhu, TRDDC, Solving Constrained Horn Clauses Using Syntax and Data

Abstract

A Constrained Horn Clause(CHC) is a logical implication involving unknown predicates. Systems of CHCs are widely used to verify programs with arbitrary loop structures. A system of CHCs is solved by finding suitable interpretations for the unknown predicates, such that it makes all implications true. These interpretations represents the program's inductive invariants. This technique proposes an algorithm based on Syntax-Guided Synthesis. For each unknown predicate, the algorithm generates a formal grammar from all relevant parts of the CHC system (i.e., using syntax). Grammars are further enriched by predicates and constants guessed from models of various unrollings of the CHC system (i.e.,using data). In this talk, I will present construction of such a grammar and how it is used iteratively to guess candidate interpretations for multiple unknown predicates.
This talk is based on following paper: Solving Constrained Horn Clauses Using Syntax and Data. FMCAD 2018 Grigory Fedyukovich, Sumanth Prabhu, Kumar Madhukar, Aarti Gupta