Madhavan Mukund, CMI, Verification of blockchains and smart contracts
Deepak DSouza, Indian Institute of Science, Bangalore, Static Analysis of Race-Free Interrupt-Driven Programs
Narayan Kumar Krishnan, CMI, Verifying Asynchronous programs with nested locks
S P Suresh, CMI, A bounded witness theorem for assertions
Vaishnavi Sundararajan, CMI, A Theory of Assertions for Dolev-Yao Models
R Ramanujam, Institute of Mathematical Sciences, Chennai, Large games and population protocols
Radhakrishnan Delhibabu, VIT Vellore, Distributed Games
Raveendra Kumar M, TCS, Coverage-based Greybox Fuzzing as Markov Chain
Ramchandra Phawade, IIT Dharwad, Free Choice Nets over Distributed Alphabets
Sumanth Prabhu S, TCS Research, Safety Proofs using Appearance and Behaviours
Animesh Basakchowdhury, TCS Research, Coverage-based Greybox Fuzzing as Markov Chain
Muqsit Azeem, TCS Research, Discovering Relational Specifications
Anantha Padmanabha, Institute of Mathematical Sciences, Satisfiability problem for Term Modal Logic
Aiswarya Cyriac, CMI, Multi-Pushdown Automata with Data
S Akshay, IIT Bombay, Knowledge transfer and information leakage in protocols
Abhisekh Sankaran, IMSc, Algorithmic metatheorems: A survey
Abdullah Abdul Khadir, CMI, Knowledge transfer and information leakage in protocols
Kissan Gauns Dessai, Govt. College,Quepem, Security Protocols to Prevent Malpractices of Summative E-examinations
Rekha Pai, IISc Bangalore, Data-Race Detection for Interrupt-Driven Kernels
Madhavan Mukund, CMI, Verification of blockchains and smart contracts (Slides)
Abstract
A blockchain is a list of records, or blocks, that grows continuously. Blockchains can be used to implement distributed ledgers that maintain a permanent and verifiable transaction history. Blockchains are typically managed by a peer-to-peer network with decentralized updates. Distributed consensus protocols are used to maintain coherence. Integrity against tampering is ensured through cryptography. Transactions are implemented as snippets of code called smart contracts. We explain the theory and technology behind blockchains and smart contracts and highlight some recent work on verification of these entities.
Deepak DSouza, Indian Institute of Science, Bangalore, Static Analysis of Race-Free Interrupt-Driven Programs (Slides)
Abstract
Narayan Kumar Krishnan, CMI, Verifying Asynchronous programs with nested locks (Slides)
Abstract
We consider asynchronous programs consisting of multiple recursive threads (modeled as pushdown systems) running in parallel. Each of the threads is equipped with a multi-set. The threads can create tasks and post them onto the multi-sets or read a task from their own. In addition, they can synchronize through a finite set of locks. We examine the decidability of the state reachability problem for this model. The problem is already known to be undecidable for a system consisting of two recursive threads (and no tasks) and we examine a decidable subclass.
R Ramanujam, Institute of Mathematical Sciences, Chennai, Large games and population protocols (Slides)
Abstract
Game theorists study large anonymous games with a large number of
players. In these games, payoffs are not associated with strategy profiles
but with strategy distributions. If, among 100 players, 30 choose a, 50 play
b and 20 choose c, all those choosing a get x_a, all those choosing b get x_b,
and so on. Such games have interesting equilibrium properties, different from
'classical games'.
Agents in a population protocol are finite automata that have no unique identifiers,
no control over their movement, and are identically programmed over a population
of unknown finite size. They communicate with other agents on a pairwise basis,
without any kind of shared memory, but simply by informing each other of their
current states and updating these states accordingly.
Intuitively, the two areas seem related, and in this talk, I introduce the two models and discuss some preliminary attempts at connecting the two.
Raveendra Kumar M, TCS, Coverage-based Greybox Fuzzing as Markov Chain (Slides)
Abstract
Ramchandra Phawade, IIT Dharwad, Free Choice Nets over Distributed Alphabets (Slides)
Abstract
Petri nets is a graphical model of distributed and concurrent systems. Free choice nets form an important subclass of Petri nets.
Another model of concurrent systems is automata--product systems--over distributed alphabets.
Sumanth Prabhu S, TCS Research, Safety Proofs using Appearance and Behaviours (Slides)
Abstract
Proving safety of programs relies principally on discovering invariants that are inductive and safe. Obtaining such invariants, therefore, has been studied widely from diverse perspectives. One recent technique is to perform guess-and-check using input program's source and SMT solver[1]. A frequency distribution is constructed based on syntax, which is used to sample candidate invariants. Candidates are then checked using an SMT solver. In this talk we will look at this technique, its limitations and how to overcome the limitations using behaviors[2][3].
Animesh Basakchowdhury, TCS Research, Coverage-based Greybox Fuzzing as Markov Chain (Slides)
Abstract
Muqsit Azeem, TCS Research, Discovering Relational Specifications (Slides)
Abstract
Formal specifications of library functions play a critical role in a number of program analysis and development tasks. We present Bach, a technique for discovering likely relational specifications from data describing input–output behavior of a set of functions comprising a library or a program. Relational specifications correlate different executions of different functions; for instance, commutativity, transitivity, equivalence of two functions, etc. Bach combines novel insights from program synthesis and databases to discover a rich array of specifications. We apply Bach to learn specifications from data generated for a number of standard libraries. Our experimental evaluation demonstrates Bach’s ability to learn useful and deep specifications in a small amount of time.
Anantha Padmanabha, Institute of Mathematical Sciences, Satisfiability problem for Term Modal Logic (Slides)
Abstract
The classical Modal logics and its First order counter parts allow us to talk about fixed number of agents, which index the modalities. Typically, we have formulas of the form \Box_i \alpha where "i" comes from a fixed finite set of agents. However, we encounter many scenarios like server-client systems, system of processes that can fork etc, where the number of agents cannot be fixed aprori. Term Modal Logic (TML) addresses this problem and gives a handle to index the modality by terms and quantify over them. In TML we can write formulas of the form \exists x \Box_x \alpha. In this talk, we shall introduce TML and discuss some tight undecidability results for the satisfiability problem and identify some decidable fragments.
Aiswarya Cyriac, CMI, Multi-Pushdown Automata with Data (Slides)
Abstract
Abdullah Abdul Khadir, CMI, Knowledge transfer and information leakage in protocols (Slides)
Abstract
Kissan Gauns Dessai, Govt. College,Quepem, Security Protocols to Prevent Malpractices of Summative E-examinations (Slides)
Abstract
Rekha Pai, IISc Bangalore, Data-Race Detection for Interrupt-Driven Kernels (Slides)
Abstract
Abhisekh Sankaran, IMSc, Algorithmic metatheorems: A survey (Slides)
Abstract
We present a (partial) survey of the area of algorithmic metatheorems. These theorems provide fixed parameter tractable (FPT) algorithms for the model checking problem, namely the problem of checking if an input structure from a given class of structures satisfies a property that is expressible in a given logic like say first order logic (FO) or monadic second order logic (MSO). The parameters in these algorithms are the size of the logical description of the property, along with (the numerical description of) some structural aspect of the input structure. We look at various well-studied classes of posets and graphs that admit such FPT algorithms and give the intuitive ideas behind the techniques involved.