Department of Computer Science and Automation Department of Computer Science and Automation, IISc, Bangalore, India Indian Institute of Science
HOME | ABOUT US | PEOPLE | RESEARCH | ACADEMICS | FACILITIES | EVENTS / SEMINARS | NEWS | CONTACT US

UPCOMING SEMINARS

Series: Department Seminar
Title: Inspiring Trust in Outsourced Computations: From Secure Chip Fabrication to Verifiable Deep Learning in the Cloud

  • Speaker: Dr. Siddharth Garg
                   NYU
                   Tandon School of Engineering
  • Date and Time: Thursday, January 18, 2018, 11:00 AM
  • Venue: CSA Seminar Hall (Room No. 254, First Floor)

Abstract
Computations are often outsourced by computationally weak clients to computationally powerful external entities. Cloud computing is an obvious example of outsourced computation; outsourced chip manufacturing to off-shore foundries or ``fabs" is another (perhaps less obvious) example. Indeed, many major semiconductor design companies have now adopted the so-called ``fabless" model. However, outsourcing raises a fundamental question of trust: how can the client ascertain that the outsourced computations were correctly performed? Using fabless chip manufacturing and ``machine-learning as a service (MLaaS)" as exemplars, this talk will highlight the security vulnerabilities introduced by outsourcing computations and describe solutions to mitigate these vulnerabilities.

First, we describe the design of "verifiable ASICs" to address the problem of secure chip fabrication at off-shore foundries. Building on a rich body of work on the ``delegation of computation" problem, we enable untrusted chips to provide run-time proofs of the correctness of computations they perform. These proofs are checked by a slower verifier chip fabricated at a trusted foundry. The proposed approach is the first to defend against arbitrary Trojan misbehaviors (Trojans refer to malicious modifications of a chip's blueprint by the foundry) while providing formal and comprehensive soundness guarantees.

Next, we examine the "MLaaS" setting, in which both the training and/or inference of machine learning models is outsourced to the cloud. We show that outsourced training introduces new security risks: an adversary can create a maliciously trained neural network (a backdoored neural network, or a BadNet) that has state-of-the-art performance on the user’s training and validation samples, but behaves badly on specific attacker-chosen inputs. We conclude by showing how the same techniques we used design ``verifiable ASICs" can be used to verify the results of neural networks executed on the cloud.

Speaker Bio:
Siddharth Garg received his Ph.D. degree in Electrical and Computer Engineering from Carnegie Mellon University in 2009, and a B.Tech. degree in Electrical Enginerring from the Indian Institute of Technology Madras. He joined NYU in Fall 2014 as an Assistant Professor, and prior to that, was an Assistant Professor at the University of Waterloo from 2010-2014. His general research interests are in computer engineering, and more particularly in secure, reliable and energy-efficient computing. In 2016, Siddharth was listed in Popular Science Magazine's annual list of "Brilliant 10" researchers. Siddharth has received the NSF CAREER Award (2015), and paper awards at the IEEE Symposium on Security and Privacy (S&P) 2016, USENIX Security Symposium 2013, at the Semiconductor Research Consortium TECHCON in 2010, and the International Symposium on Quality in Electronic Design (ISQED) in 2009. Siddharth also received the Angel G. Jordan Award from ECE department of Carnegie Mellon University for outstanding thesis contributions and service to the community. He serves on the technical program committee of several top conferences in the area of computer engineering and computer hardware, and has served as a reviewer for several IEEE and ACM journals.

Host Faculty: Prof. Vinod Ganapathy & Prof. Aditya Gopalan (ECE)

Video Archive Go Top

 

PAST SEMINARS

Series: M.Sc. (Engg) Thesis Defense
Title: A Fine-Grained Dynamic Information Flow Analysis for Android Apps

  • Speaker: Mr. Shyam Sankaran
                   M.Sc. (Engg) student
                   Dept. of CSA
                   IISc
  • Faculty Advisor: Prof. Aditya S Kanade
  • Date and Time: Monday, January 15, 2018, 10:00 AM
  • Venue: CSA Seminar Hall (Room No. 254, First Floor)

Abstract
Android has been steadily gaining popularity ever since its launch in 2008. One of the major factors for this is the easy availability of a large variety of apps. They range from simple apps such as calculator apps to apps which can help people maintain their schedules and thus manage many aspects of their lives. In addition, a lot of free apps are available to the user thanks to the power of in-app purchases and advertisements. However, these also raise many security concerns. Apps are privy to a lot of private information regarding the user, such as his contacts, location, etc. It is essential to ascertain that apps do not leak such information to untrustworthy entities. In order to solve this problem, there have been many static and dynamic analyses which aim to track private data accessed or generated by the app to its destination. Such analyses are commonly known as Information Flow analyses. Dynamic analysis techniques, such as TaintDroid, tracks private information and alerts the user when it is accessed by specific API calls. However, they do not track the path taken by the information, which can be useful in debugging and validation scenarios.

The first key contribution of this thesis is a model to perform dynamic information flow analysis, inspired by FlowDroid and TaintDroid, which can retain path information of sensitive data in an efficient manner. The model instruments the app and uses path-edges to track the information flows during a dynamic run. We describe the data structure and transfer functions used, and the reasons for its design based on the challenges posed by the Android programming model and efficiency requirements. The second key contribution is the capability to trace the path taken by the sensitive information based on the information obtained during the analysis, as well as the capability to complement static analyses such as FlowDroid with the output of this analysis. The tests conducted on the implemented model using DroidBench and GeekBench 3 show the precision and soundness of the analysis, and a performance overhead of 25% while real-world apps show negligible lag. All leaks seen in DroidBench where successfully tracked and were verified to be true positives. We tested the model on 10 real-world apps where we find on average about 16.4% of the total path-edges found by FlowDroid.

Video Archive Go Top

 

Series: M.Sc. (Engg) Thesis Defense
Title: Fully Resilient Non-Interactive ID-Based Hierarchical Key Agreement.

  • Speaker: Mr. Mayank Tiwari
  • Faculty Advisor: Prof. Sanjit Chatterjee
  • Date and Time: Thursday, January 11, 2018, 11:00 AM
  • Venue: CSA Seminar Hall (Room No. 254, First Floor)

Abstract
Fully Resilient Non-Interactive Id-based Hierarchical Key Agreement Non-Interactive Key Agreement (NIKA) is a cryptographic primitive which allows two parties to agree on a shared key without any interaction. Identity-based Non-Interactive Key Agreement (ID-NIKA) allows each party to compute shared secret key using its own secret key and the peer’s identity. ID-NIKA can be used to establish shared secret keys in Ad-hoc networks using minimal battery power and communication.

Mobile Ad-hoc NETwork (MANET) is a network of mobile and moderately resource constrained devices communicating through a wireless medium. Examples of standard MANET devices are laptops, cellphones etc. Due to the inherent characteristics like mobility, dynamic topology and lack of centralized infrastructure, MANETs face some serious security issues. We are particularly interested about ID-NIKA in MANETs. This is of crucial interest for secure communication between two nodes in MANETs.

In 2008, Gennaro et al. introduced a scheme called Hybrid Hierarchical Key Agreement Scheme (HH-KAS). HH-KAS uses a linear hierarchical key agreement scheme at the non-leaf levels and a key agreement scheme due to Sakai et al. (referred as SOK-KAS) at the leaf level. HH-KAS is (i) non-interactive, (ii) identity based, (iii) hierarchical and is (iv) fully resilient against node compromises at leaf level and resilient against node compromises upto certain threshold values in non-leaf levels. Thus one can say that HH-KAS is partially resilient against node compromises. In their paper the authors claim that there is no key agreement scheme for MANETs in the literature, with all above four properties. This was motivated as an interesting open problem in this area.

Guo et al. proposed a scheme known as Strong Key Agreement Scheme (SKAS) in 2011. The authors claimed it a potential solution to the open problem posed by Gennaro et al. in their work. However, in 2014, Zhu et al. showed a concrete attack on SKAS. This attack makes SKAS practically useless for real life applications.

Our main contribution is a hybrid scheme using two already existing schemes. Our scheme uses a deterministic key pre-distribution scheme by Lee and Stinson termed as Basic Id One-way function Scheme (BIOS) at level 1 (where root is at level 0). Beyond level 1, we use SOK-KAS for key agreement. We refer our scheme as BIOS-SOK key agreement. BIOS and SOK schemes satisfy properties (i), (ii) and (iv) but none of them is hierarchical in nature. In our work we have made an amalgam of both schemes which is hierarchical in nature. Thus, BIOS-SOK scheme satisfies (i), (ii), (iii) and is also fully resilient against arbitrary number of node compromises at any level.

BIOS-SOK scheme also possesses the benefits of low space requirement, low shared key computation time and better scalability for many real-life applications when compared with the scheme of Gennaro et al. In HH-KAS, the key agreement is carried out only at the leaf level. In BIOS-SOK scheme, any two nodes in the hierarchy (at same or different levels) can compute shared secret key. We also provide a rigorous security analysis for our scheme in a stronger security model compared to the security model used for HH-KAS.

Video Archive Go Top

 

Series: Department Seminar
Title: Two Modeling Primitives for Computer Aided Geometric Design

  • Speaker: Dr Jinesh Machchhar
                   Post doctoral Fellow, Technion
  • Date and Time: Wednesday, January 10, 2018, 4:00 PM
  • Venue: CSA Seminar Hall (Room No. 254, First Floor)

Abstract
Computer Aided Geometric Design concerns development of algorithms and accompanying software, towards design of parts and structures with a high degree of numerical precision. Target application domains include design of automobiles, aircrafts and buildings, among others. In this talk we discuss two kernel level modeling primitives. First, we propose a comprehensive algorithmic framework for computation of solid sweeps. This involves computing the boundary of the swept volume generated by moving the input solid along the input one-parameter-family of rigid motions in three dimensional space. In particular, we discuss local issues such as the parametrization of the boundary surface, detection and elimination of self-intersections, as well as global issues such as body-check and the topological data associated with the swept volume. Several examples from a prototype implementation in the ACIS modeling kernel will be shown. Applications include CNC machining verification, product handling and collision detection. Second, we demonstrate a robust computational interface for precise modeling of microstructures towards 3D printing. This is achieved through functional composition of B-spline functions and allows separate design of the micro and the macro structures of an object. In particular, we demonstrate construction of recursive, fractal-like microstructures which are composed of trivariate tiles with C0-discontinuities. Applications include design of porous and composite materials. This is joint work with Milind Sohoni, Bharat Adsul and Gershon Elber.

Speaker Bio:
Jinesh Machchhar is a post-doctoral fellow in the faculty of computer science at Technion-Israel Institute of Technology. He obtained his Ph.D. from IIT Bombay under the guidance of Prof. Milind Sohoni and Prof. Bharat Adsul in 2015. He did his M.Tech from IIT Bombay and his bachelor of engineering from South Gujarat University. His research interests include geometric modeling, surface design and analysis, and software development for computer aided design and manufacturing.

Host Faculty: Prof. Matthew Jacob

Video Archive Go Top

 

Series: Department Seminar
Title: Single and Multiobjective Evolutionary Fuzzy Clustering

  • Speaker: Prof. Ujjwal Maulik
                   Professor and Head of the Department of Computer Science and Engineering
                   Jadavpur University, Kolkata
  • Date and Time: Wednesday, January 10, 2018, 11:30 AM
  • Venue: CSA Seminar Hall (Room No. 254, First Floor)

Abstract
Data clustering is a popular unsupervised data mining tool that is used for partitioning a given data set into homogeneous groups based on some similarity/dissimilarity metric. There are several single objective clustering algorithms available and popular in the literature including KMean and FCM. Although both KMean and FCM are very popular algorithms, they may stuck to local optima depending on the choice of initial cluster centers. In this lecture first we will demonstrate how Metaheuristic techniques can be used to solve the problem of KMean/FCM. Result will be demonstrated for pixel classification of satellite images.

In the second part of the problem we will discuss Multiobjective clustering, in which multiple objective functions are simultaneously optimized. Selecting one solution from the set of Pareto Optimal solutions is always a critical issue. We will also discuss how machine learning techniques like Support Vector Machine (SVM) can be used to combine the Pareto Optimal solutions to evolve a better solution. The result will be demonstrated for classification of Gene Micro Array Data.

Speaker Bio:
Dr. Ujjwal Maulik is a Professor in the Department of Computer Science and Engineering, Jadavpur University. Currently, he is also the Chair of the department. In the past, Dr. Maulik has worked at Los Alamos National Laboratory (USA), Tsinghua University (China), University of Heidelberg (Germany), German Cancer Research Center (DKFZ), and International Center of Theoretical Physics (Italy) among several other institutes. He is the recipient of Govt. of India BOYSCAST fellowship, Alexander Von Humboldt Fellowship for Experienced Researchers and Senior Associate of ICTP, Italy. He is also a Fellow of Indian National Academy of Engineering (INAE). His research interests include Pattern Recognition, Computational Intelligence, Computational Biology, Combinatorial Optimization, Data Mining and Social Network.

Host Faculty: Prof. Y Narahari and Dr. Chandan Saha

Video Archive Go Top

 

Series: Department Seminar
Title: Visual Cortex on Silicon

  • Speaker: Prof. Chita Das, Penn State University
  • Date and Time: Tuesday, January 09, 2018, 10:00 AM
  • Venue: CSA Seminar Hall (Room No. 254, First Floor)

Abstract
Our visual cortex is highly sophisticated in terms of processing dynamically changing scenes with minimal energy consumption. The objective of this multidisciplinary project is to explore the feasibility of designing an end-to-end visual cortex system on silicon so that it can be integrated with a mobile platform and subsequently in the IoT ecosystem. This talk covers an overall view of the complete design space covering the understanding of the human cognitive system, mapping it to vision algorithms, exploring the hardware design alternatives, and the human interface issues for three application domains – visually impaired, driver assistance and augmented reality. The talk will conclude with some architectural design challenges for designing an energy-efficient visual cortex system and extending it further to neuromorphic architectures.

Speaker Bio:
Chita Das is the Department Head and a Distinguished Professor of Computer Science and Engineering at the Pennsylvania State University. His main areas of interest include CMPs and many core architectures, GPUs, handhelds, performance evaluation, fault-tolerant computing, and Clouds/datacenters. In particular, he has worked extensively in the area of design and analysis of interconnection networks/on-chip interconnects. He is a Fellow of the IEEE.

Host Faculty: R. Govindarajan

Video Archive Go Top

 

Series: Department Seminar
Title: Learning Combinatorial Structures.

  • Speaker: Dr. Swati Gupta
  • Date and Time: Monday, January 08, 2018, 4:00 PM
  • Venue: CSA Lecture Hall (Room No. 117, Ground Floor)

Abstract
At the heart of most algorithms today, there is an optimization engine trying to provide the best decision with partial information observed thus far in time, the so-called problem of online learning. Often it becomes difficult to find near-optimal solutions to these problems due to their inherent combinatorial structure that leads to certain computational bottlenecks, for instance, computing Bregman projections for online mirror descent and its variants. Motivated by these bottlenecks, we consider three fundamental convex and combinatorial optimization problems. First, we provide a conceptually simple algorithm to minimize separable convex functions over submodular base polytopes. For cardinality-based submodular functions, we show the current fastest-known running time of O(n(log n+d)), where n is the size of the ground set and d is the number of distinct values of the submodular function (d<=n). Next, we consider the problem of movement along a line while staying feasible in submodular polytopes. The use of the discrete Newton’s method for this line search problem is natural, but no strongly polynomial bound on its number of iterations was known. We solve this open problem by providing a quadratic bound of O(n2), resulting in a running time improvement by at least n6 over the state of the art. Finally, we show how efficient counting methods can be used for convex minimization. This is joint work with Michel Goemans and Patrick Jaillet.

Speaker Bio:
Swati Gupta is currently a Research Fellow at the Simons Institute for the Theory of Computing, UC Berkeley. She obtained her doctoral degree from the Operations Research Center at MIT in 2017 and was jointly advised by Michel Goemans and Patrick Jaillet. She graduated from Indian Institute of Technology (IIT), Delhi, in 2011 with dual Bachelors and Masters degree in Computer Science and Engineering. She won the Google Women in Engineering Award in 2011, special recognition from INFORMS Computing Society in 2016 and was a finalist in the INFORMS Service Science student paper award in 2016. Starting July 2018, Swati Gupta will be an assistant professor at the Industrial and Systems Engineering department at Georgia Institute of Technology.

Host Faculty: Dr. Anand Louis

Video Archive Go Top

 

Series: Ph.D. Colloquium
Title: Stochastic approximation with set-valued maps and Markov noise : Theoretical foundations and applications.

  • Speaker: Mr. Vinayaka G. Yaji
  • Faculty Advisor: Prof Shalabh Bhatnagar
  • Date and Time: Monday, January 08, 2018, 11:30 AM
  • Venue: CSA Faculty Room, (Room No. 101, Ground floor)

Abstract
Stochastic approximation algorithms produce estimates of a desired solution using noisy real world data. Introduced by Robbins and Monro, in 1951, stochastic approximation techniques have been instrumental in the asymptotic analysis of several applications in adpative aglorithms in learning, signal processing and control. A popular method for the analysis of stochastic approximation schemes is the dynamical systems approach or the o.d.e. method introduced by Ljung and developed further extensively by Benaim and Hirsch.

We build upon the works of Benaim et.al. and Bhatnagar et.al., and present the asymptotic analysis of stochastic approximation schemes with set-valued drift functions and non-additive Markov noise. The frameworks studied by us are under the weakest set of assumptions and encompass a majority of the methods studied to date. We first study the asymptotic behavior of stochastic approximation schemes with set-valued drift function and non-additive iterate-dependent Markov noise. We show that a linearly interpolated trajectory of such a recursion is an asymptotic pseudo-trajectory for the flow of a limiting differential inclusion obtained by averaging the set-valued drift function of the recursion with respect to the stationary distributions of the Markov noise. The limit set theorem by Benaim is then used to characterize the limit sets of the recursion in terms of the dynamics of the limiting differential inclusion. The analysis presented allows us characterize the asymptotic behavior of controlled stochastic approximation, subgradient descent, approximate drift problem and analysis of discontinuous dynamics all in the presence of non-additive iterate-dependent Markov noise.

Next we present the asymptotic analysis of a stochastic approximation scheme on two timescales with set-valued drift functions and in the presence of non-additive iterate-dependent Markov noise. It is shown that the recursion on each timescale tracks the flow of a differential inclusion obtained by averaging the set-valued drift function in the recursion with respect to a set of measures which take into account both the averaging with respect to the stationary distributions of the Markov noise terms and the interdependence between the two recursions on different timescales.

Finally we study the behavior of stochastic approximation schemes with set-valued maps in the absence of a stability guarantee. We prove that after a large number of iterations if the stochastic approximation process enters the domain of attraction of an attracting set it gets locked into the attracting set with high probability. We demonstrate that the above result is an effective instrument for analyzing stochastic approximation schemes in the absence of a stability guarantee, by using it to obtain an alternate criterion for convergence in the presence of a locally attracting set for the mean field and by using it to show that a feedback mechanism, which involves resetting the iterates at regular time intervals, stabilizes the scheme when the mean field possesses a globally attracting set, thereby guaranteeing convergence. Our results build on the works of Borkar, Andrieu et al. and Chen et al., by allowing for the presence of set-valued drift functions.

Video Archive Go Top

 

Series: Department Seminar
Title: Optimization for derandomization: polynomial identity testing, geodesically convex optimization and more

  • Speaker: Dr Ankit Garg
                    Postdoctoral Researcher, Microsoft Research New England, Boston
  • Date and Time: Monday, January 08, 2018, 10:00 AM
  • Venue: CSA Lecture Hall (Room No. 117, Ground Floor)

Abstract
Randomness plays an important role across scientific disciplines. In theoretical computer science, there is a large body of work trying to understand the role of randomness in computation. An important part in this quest is the polynomial identity testing question which asks if one can test identities deterministically. In this talk, I will talk about deterministic identity testing of a special class of polynomials using tools from optimization. The class of problems that we solve form an amazing web of connections across areas such as geodesically convex optimization, quantum information theory, representation theory, non-commutative algebra and functional analysis. I will also outline applications to these areas. The talk will be based on several joint works with Zeyuan Allen-Zhu, Peter Burgisser, Leonid Gurvits, Yuanzhi Li, Rafael Oliveira, Michael Walter and Avi Wigderson.

Host Faculty: Prof. Matthew Jacob

Video Archive Go Top

 

Series: Ph.D. Colloquium
Title: Typestates and Beyond: Verifying Rich Behavioral Properties Over Complex Programs

  • Speaker: Ashish Mishra
  • Faculty Advisor: Y.N. Srikant
  • Date and Time: Friday, January 05, 2018, 4:00 PM
  • Venue: CSA Lecture Hall (Room No. 117, Ground Floor)

Abstract
Statically verifying behavioral properties of programs is an important research problem. Type systems are the most prevalently used static, light-weight verification systems for verifying certain properties of programs. Unfortunately, simple types are inadequate at verifying many behavioral/dynamic properties of programs. Typestates can tame this inadequacy of simple types by associating each type in a programming language with a state information. However, there are two major challenges in statically analyzing and verifying typestate properties over programs.

The first challenge may be attributed to ``increasing complexity of programs''. The state-of-the-art static typestate analysis works still cannot handle formidably rich programming features like asynchrony, library calls and callbacks, concurrency, etc. The second challenge may be attributed to ``complexity of the property being verified''. The original and the current notion of typestates can only verify a property definable through a finite-state abstraction, and are inadequate to verify useful but richer and non-regular program properties. For example, using classical typestates we can verify a property like, ``pop be called on a stack only after a push operation'', but we cannot verify a non-regular program property like, ``number of push operations should be at least equal to the number of pop operations''. Currently, these behavioral properties are mostly verified/enforced by programmers at runtime via explicit checks. Unfortunately, these runtime checks are costly, error-prone, and lay an extra burden on the programmer.

In this thesis we take small steps towards tackling both these challenges. Addressing complex program features, we present an asynchrony-aware static analysis, taking Android applications as our use case. We provide a formal semantics for Android asynchronous control flow, use these semantics to introduce an intermediate program representation for Android applications, called the Android Inter Component Control Flow Graph (AICCFG), and develop an asynchrony-aware interprocedural static analysis framework for Android applications. We use this framework to develop a static typestate analysis to capture Android resource API usage protocol violations. We present a set of benchmark applications for different resource types, and empirically compare our typestate analysis with the state-of-the-art synchronous static analyses for Android applications.

Addressing the challenges associated with increasing complexity of properties, we present an expressive notion of typestates called, Parameterized typestates (p-typestates). p-typestates associate an extra Pressburger definable property along with states of regular typestates. This allows p-typestates to express many useful non-regular properties. We present a dependent type system for p-typestates and present a simple typestate-oriented language incorporating p-typestates. Further, typechecking such rich p-typestate properties requires a programmer to provide invariants for loops and recursive structures. Unfortunately, providing these invariants is a non-trivial task even for expert programmers. To solve this problem, we present a simple and novel loop invariant calculation approach for Pressburger definable systems. We encode a number of real world programs in our dependently-typed language to verify several rich and non-regular properties.

Finally we discuss several possible extensions of our thesis along both these directions.

Speaker Bio:
Ashish Mishra is a Ph.D student in the CSA department.

Host Faculty: Y.N. Srikant

Video Archive Go Top

 

Series: M.Sc. (Engg) Thesis Defense
Title: An improved lower bound for multi-r-ic depth four circuits as a function of the number of input variables

  • Speaker: Sumant Hegde
  • Faculty Advisor: Dr. Chandan Saha
  • Date and Time: Friday, January 05, 2018, 11:00 AM
  • Venue: CSA Conference Room (Room No. 225, First Floor)

Abstract
In this work we study the multi-r-ic formula model introduced by Kayal and Saha (2015) and improve upon the lower bound for multi-r-ic depth four circuits given in the work by Kayal, Saha and Tavenas (2016) [KST16], when viewed as a function of the number of input variables N. The improvement leads to superpolynomial lower bounds for values of r significantly higher than what is known from prior works.

A (syntactically) multi-r-ic formula is an arithmetic formula in which the formal degree with respect to every variable is at most r at every gate. The formal degree of an input gate with respect to a variable x is defined to be 1 if the gate is labelled with x and 0 if it is labelled with a field element or a different variable. The formal degree of a sum (respectively, product) gate with respect to x is defined as the maximum (respectively, sum) of the formal degrees of its children with respect to x. Naturally, a multi-r-ic formula computes a polynomial with individual degree of every variable bounded by r.

Multi-r-ic formulas are a natural extension of the relatively well-studied multilinear formulas in the work by Raz (2009) and Raz and Yehudayoff (2009) [RY09]. In this work, we focus on multi-r-ic formulas that compute multilinear polynomials. They are interesting because they allow the formal degree of the formula to be as high as r times the number of underlying variables. This gives extra room for ‘clever’ cancellations of the high degree components inside the formula thereby making this type of formulas harder to analyse (as formula homogenization is not known to be doable without blowing up the size superpolynomially unless degree is very small, as Raz (2010) showed). Most lower bound proofs in the literature operate under the restriction of low formal degree or multilinearity (as in the works by Raz (2009), [RY09], Kayal, Saha and Saptharishi (2014) and Kayal, Limaye, Saha and Srinivasan (2014)). In this light, multi-r-ic formulas computing multilinear polynomials form a reasonable intermediate model to study in order to gain some insight on how to deal with high formal degree in general formulas. Another motivation for understanding the high formal degree case better (even at depth three) comes from the depth reduction result by Gupta, Kamat, Kayal and Saptharishi (2013).

With the aim of making progress on multi-r-ic formula lower bound, [KST16] gave a (N/(d·r^2))^Ω(√(d/r)) lower bound for multi-r-ic depth four formulas computing the N-variate Iterated Matrix Multiplication (IMM) polynomial of degree d. As a function of N, the lower bound is at most 2^Ω(√(N/r^3)) when d = Θ(N/r^2). In this thesis, our focus is on getting multi-r-ic depth four formulas with larger r into the arena of models that provenly admit a superpolynomial lower bound. In [KST16], r can be at most N^(1/3) for the bound to remain superpolynomial. Our result (stated below) gives a superpolynomial lower bound for multi-r-ic depth four formulas where r can be as high as (N·log N)^(0.9).

Theorem: Let N, d, r be positive integers such that 0.51·N ≤ d ≤ 0.9·N and r ≤ (N·log N)^(0.9). Then there is an explicit N-variate degree-d multilinear polynomial in VNP such that any multi-r-ic depth four circuit computing it has size 2^Ω(√(N·(log N)/r)).

The theorem yields a better lower bound than that of [KST16], when viewed as a function of N. Also, the bound matches the best known lower bound (as a function of N) for multilinear (r = 1) depth four circuits, given by [RY09], which is 2^Ω(√(N·log N)).

The improvement is obtained by analysing the shifted partials dimension (SPD) of an N-variate polynomial in VNP (as opposed to a VP polynomial in [KST16]) of high degree range of Θ(N), and comparing it with the SPD of a depth four multi-r-ic circuit. In [KST16] a variant of shifted partials, called shifted skewed partials, is critically used to analyse the IMM polynomial (which is in VP). We observe that SPD (without “skew”) is still effective for the Nisan-Wigderson polynomial (which is in VNP), and yields a better lower bound as a function of N when degree d is naturally chosen to be high.

Our analysis gives a better range for r and a better lower bound in the high degree regime, not only for depth four multi-r-ic circuits but also for the weaker models: multi-r-ic depth three circuits and multi-r-ic depth four circuits with low bottom support. These (weaker) models are instrumental in gaining insight about general depth four multi-r-ic circuits, both in [KST16] and our work.

Video Archive Go Top

 

Series: Department Seminar
Title: On The Unreasonable Effectiveness of Boolean SAT Solvers

  • Speaker: Prof. Vijay Ganesh
                   University of Waterloo
                   Canada
  • Date and Time: Friday, January 05, 2018, 11:00 AM
  • Venue: CSA Multimedia Class (Room No. 252, First Floor)

Abstract
Modern conflict-driven clause-learning (CDCL) Boolean SAT solvers routinely solve very large industrial SAT instances in relatively short periods of time. This phenomenon has stumped both theoreticians and practitioners since Boolean satisfiability is an NP-complete problem widely believed to be intractable. It is clear that these solvers somehow exploit the structure of real-world instances. However, to-date there have been few results that precisely characterize this structure or shed any light on why these SAT solvers are so efficient. In this talk, I will present results that provide a deeper empirical understanding of why CDCL SAT solvers are so efficient, which may eventually lead to a complexity-theoretic result. Our results can be divided into two parts. First, I will talk about structural parameters that can characterize industrial instances and shed light on why they are easier to solve even though they may contain millions of variables. Second, I will talk about internals of CDCL SAT solvers, and describe why they are particularly suited to solve industrial instances.

Speaker Bio:
Dr. Vijay Ganesh is an assistant professor at the University of Waterloo since 2012. Prior to that he was a research scientist at MIT, and completed his PhD in computer science from Stanford University in 2007. Vijay's primary area of research is the theory and practice of automated reasoning aimed at software engineering, formal methods, security, and mathematics. In this context he has led the development of many SAT/SMT solvers, most notably, STP, The Z3 string solver, MapleSAT, and MathCheck. He has also proved several decidability and complexity results relating to the satisfiability problem for various mathematical theories. For his research, he has won over 21 awards, honors, and medals including an ACM Test of Time Award at CCS 2016, an Ontario Early Researcher Award 2016, two Google Faculty Research Awards in 2011 and 2013, and a Ten-Year Most Influential Paper citation at DATE 2008.

Host Faculty: Prof. Vinod Ganapathy

Video Archive Go Top

 

Series: I. G. Sarma Memorial Lecture Series
Title: Computation as a Scientific Weltanschauung

  • Speaker: Professor Christos Papadimitriou
                   Columbia University
  • Date and Time: Thursday, January 04, 2018, 4:00 PM
  • Venue: Faculty Hall, Indian Institute of Science

Abstract
Looking at the natural, life, and social sciences from the point of view of computation often results in unexpected insights, and progress in important problems. I will focus on some recent work in the life sciences: Evolution of a population through sexual reproduction can be rethought of as a repeated game between genes played through a well known, and powerful, algorithm, while selection, when acting in gene combinations instead of genes alone, can take exponentially long to fixate. Finally, experiments on the formation of stable memories in the human medial temporal lobe, and the associations between memories, can be explained through a random graph model and a connection to the sparsest k-subgraph problem.

Speaker Bio:
Christos H. Papadimitriou is the Donoval Family Professor of Computer Science at Columbia University. Before joining Columbia this year, he taught at Harvard, MIT, NTU Athens, Stanford, UCSD, and at Berkeley since 1995. He has written many books and articles on the theory of algorithms and complexity, and its applications to optimization, databases, control, AI, robotics, economics and game theory, the Internet, evolution, and the brain. He holds a PhD from Princeton, and honorary doctorates from nine universities. He is a member of the National Academy of Sciences of the US, the American Academy of Arts and Sciences, and the National Academy of Engineering, and is a recipient of the Knuth prize, the Gödel prize, the Kalai prize for CS in Game Theory, the EATCS award, and the von Neumann medal. He has also written three novels: "Turing", " Logicomix" and his latest "Independence" (2017).

Video Archive Go Top

 

Series: Department Seminar
Title: Derandomizing the Isolation Lemma and Parallel algorithms

  • Speaker: Dr Rohit Gurjar
                   Post doctoral Fellow, Center for the Mathematics of Information, Caltech
  • Date and Time: Thursday, January 04, 2018, 10:00 AM
  • Venue: CSA Lecture Hall (Room No. 117, Ground Floor)

Abstract
To understand the power of randomization is one of the fundamental questions in theoretical computer science. In particular, we want to know if every problem with an efficient randomized algorithm also has a deterministic one, without much loss in efficiency. One of the widely used tools in randomized algorithms is the Isolation Lemma of Mulmuley-Vazirani-Vazirani. It states that for any family of subsets of a set, if the each element of the set is assigned a random weight from a small range, then with high probability the family has a unique minimum weight set. One of the many applications of the Isolation lemma is a randomized parallel algorithm for the perfect matching problem.

Derandomizing the Isolation lemma, that is, to deterministically construct weights with the isolating property, has been an interesting open question. In a series of works, we derandomized the isolation lemma for many interesting families of sets. Among many implications of these results are deterministic parallel (quasi-NC) algorithms for bipartite matching and linear matroid intersection and, a solution to some polynomial identity testing questions. The most general setting where our technique works is when the polytope corresponding to the family has all its faces defined by totally unimodular equations. The talk will give an overview of these results and some possible future directions.

Based on joint works with Stephen Fenner, Thomas Thierauf, Nisheeth Vishnoi.

Host Faculty: Prof. Matthew Jacob

Video Archive Go Top

 

Series: Department Seminar
Title: Acceleration of FPGA-SoC-ASIC Design and Verification using Model Based Design and HDLCoder

  • Speaker: Kiran Kintali
                   MathWorks, USA
  • Date and Time: Wednesday, January 03, 2018, 4:00 PM
  • Venue: CSA Seminar Hall (Room No. 254, First Floor)

Abstract
Model based design using MATLAB and Simulink helps accelerate ASIC/FPGA/SoC design and verification using HDLCoder workflow. HDL Coder™ generates portable, synthesizable Verilog® and VHDL® code from MATLAB® functions, Simulink® models, and Stateflow® charts. The generated HDL code can be used for FPGA programming or ASIC prototyping and design. HDL Coder provides a workflow advisor that automates the programming of Xilinx® and Intel® FPGAs. You can control HDL architecture and implementation, highlight critical paths, and generate hardware resource utilization estimates. HDL Coder provides traceability between your Simulink model and the generated Verilog and VHDL code, enabling code verification for high-integrity applications adhering to DO-254 and other standards.

Apart from introducing HDLCoder, this talk will highlight some of the challenges in building a high-level language compiler like HDLCoder and translation from MATLAB (a control flow based programming language) and Simulink (a data flow based algorithm design environment) to C/C++ and RTL (VHDL/Verilog/System Verilog) to target and program software and hardware components in SoCs.

Speaker Bio:
Kiran Kintali manages the HDL Coder™ product development team at MathWorks. He is one of the principal developers of HDL Coder and joined MathWorks in 2003 to build compiler technology for automatic HDL code generation from MATLAB and Simulink to target FPGAs and ASICs. Kiran has over 15 patents related to automatic code generation techniques, compiler optimizations, and fixed-point conversion and native floating point code generation. Prior to joining MathWorks, he worked at semiconductor companies Conexant and Zilog, developing their embedded software compiler tool chain. He holds an M.S. in electrical engineering from National Institute of Technology, Surathkal, India.

Host Faculty: Y.N. Srikant

Video Archive Go Top

 

Series: Ph.D. Colloquium
Title: Stochastic Approximation with Markov Noise: Analysis and applications in reinforcement learning

  • Speaker: Prasenjit Karmakar
  • Faculty Advisor: Prof. Shalabh Bhatnagar
  • Date and Time: Wednesday, January 03, 2018, 2:00 PM
  • Venue: CSA Seminar Hall (Room No. 254, First Floor)

Abstract
Stochastic approximation algorithms are sequential non-parametric methods for finding a zero or minimum of a function in the situation where only the noisy observations of the function values are available. Two time-scale stochastic approximation algorithms consist of two coupled recursions which are updated with different (one is considerably smaller than the other) step sizes which in turn facilitate convergence for such algorithms.

1) We present for the first time an asymptotic convergence analysis of two time- scale stochastic approximation driven by 'controlled' Markov noise. In particular, the faster and slower recursions have non-additive controlled Markov noise components in addition to martingale difference noise. We analyze the asymptotic behavior of our framework by relating it to limiting differential inclusions in both time scales that are defined in terms of the ergodic occupation measures associated with the controlled Markov processes. 2) Using a special case of our results, we present a solution to the off-policy convergence problem for temporal-difference learning with linear function approximation.

3) One of the important assumption in the earlier analysis is the point-wise boundedness (also called the 'stability') of the iterates. However, finding sufficient verifiable conditions for this is very hard when the noise is Markov as well as when there are multiple timescales . We compile several aspects of the dynamics of stochastic approximation algorithms with Markov iterate-dependent noise when the iterates are not known to be stable beforehand. We achieve the same by extending the lock-in probability (i.e. the probability of convergence to a specific attractor of the limiting o.d.e. given that the iterates are in its domain of attraction after a sufficiently large number of iterations (say) n 0 ) framework to such recursions. Specifically, with the more restrictive assumption of Markov iterate-dependent noise supported on a bounded subset of the Euclidean space we give a lower bound for the lock- in probability. We use these results to prove almost sure convergence of the iterates to the specified attractor when the iterates satisfy an 'asymptotic tightness' condition. This, in turn, is shown to be useful in analyzing the tracking ability of general 'adaptive' algorithms. Additionally, we show that our results can be used to derive a sample complexity estimate of such recursions, which then can be used for step-size selection.

4) Finally, we obtain the first informative error bounds on function approximation for the policy evaluation algorithm proposed by Basu et al. when the aim is to find the risk-sensitive cost represented using exponential utility. We also give examples where all our bounds achieve the “actual error” whereas the earlier bound given by Basu et al. is much weaker in comparison. We show that this happens due to the absence of difference term in the earlier bound which is always present in all our bounds when the state space is large. Additionally, we discuss how all our bounds compare with each other.

Video Archive Go Top

 

Series: Department Seminar
Title: The Parameterized Complexity of Matrix Factorization Problems

  • Speaker: Prof. David Woodruff
  • Date and Time: Friday, December 29, 2017, 3:00 PM
  • Venue: CSA Seminar Hall (Room No. 254, First Floor)

Abstract
This will be an overview talk on several NP-hard variants of low rank approximation, including non-negative low rank approximation, weighted low rank approximation, and ell_1-low rank approximation. These problems have important applications in machine learning and numerical linear algebra. I will discuss various ways of coping with hardness for these problems, such as via approximation, parameterized complexity, and through bicriteria solutions.

Parts of this talk are based on my work with Ilya Razenshteyn, and Zhao Song (STOC '16) and with Zhao Song and Peilin Zhong (STOC '17).

Speaker Bio:
David Woodruff received his Ph.D. from MIT in 2007​,​​ worked as a research scientist at IBM Almaden ​till 2017, and has recently joined the faculty of Carnegie Mellon University. His research interests are in big data, including communication complexity, compressed sensing, data streams, machine learning, and numerical linear algebra. He is the author of the book “Sketching as a Tool for Numerical Linear Algebra”. He received best paper awards in STOC and PODS, and the Presburger award.

Host Faculty: Dr. Arnab Bhattacharyya

Video Archive Go Top

 

Series: M.Sc. (Engg) Thesis Defense
Title: Supervised Classification of Missense Mutations as Pathogenic or Tolerated using Ensemble Learning Methods.

  • Speaker: Rashmi Balasubramanyam
  • Faculty Advisor: Prof. Chiranjib Bhattacharyya
  • Date and Time: Friday, December 29, 2017, 10:00 AM
  • Venue: CSA Seminar Hall (Room No. 254, First Floor)

Abstract
Missense mutations account for more than 50% of the mutations known to be involved in human inherited diseases. Missense classification is a challenging task that involves sequencing of the genome, identifying the variations, and assessing their deleteriousness. This is a very laborious, time and cost intensive task to be carried out in the laboratory. Advancements in bioinformatics have led to several large-scale next-generation genome sequencing projects, and subsequently the identification of genome variations. Several studies have combined this data with information on established deleterious and neutral variants to develop machine learning based classifiers.

There are significant issues with the missense classifiers due to which missense classification is still an open area of research. These issues can be classified under two broad categories: (a) Dataset overlap issue - where the performance estimates reported by the state-of-the-art classifiers are overly optimistic as they have often been evaluated on datasets that have significant overlaps with their training datasets. Also, there is no comparative analysis of these tools using a common benchmark dataset that contains no overlap with the training datasets, therefore making it impossible to identify the best classifier among them. Also, such a common benchmark dataset is not available. (b) Inadequate capture of vital biological information of the protein and mutations - such as conservation of long-range amino acid dependencies, changes in certain physico-chemical properties of the wild-type and mutant amino acids, due to the mutation. It is also not clear how to extract and use this information. Also, some classifiers use structural information that is not available for all proteins.

In this study, we compiled a new dataset, containing around 2 - 15% overlap with the popularly used training datasets, with 18,036 mutations in 5,642 proteins. We reviewed and evaluated 15 state-of-the-art missense classifiers - SIFT, PANTHER, PROVEAN, PhD-SNP, Mutation Assessor, FATHMM, SNPs&GO, SNPs&GO-3D, nsSNPAnalyzer, PolyPhen-2, SNAP, MutPred, PON-P2, CONDEL and MetaSNP, using the six metrics - accuracy, sensitivity, specificity, precision, NPV and MCC. When evaluated on our dataset, we observe huge performance drops from what has been claimed. Average drop in the performance for these 13 classifiers are around 15% in accuracy, 17% in sensitivity, 14% in specificity, 7% in NPV, 24% in precision and 30% in MCC. With this we show that the performance of these tools is not consistent on different datasets, and thus not reliable for practical use in a clinical setting.

As we observed that the performance of the existing classifiers is poor in general, we tried to develop a new classifier that is robust and performs consistently across datasets, and better than the state-of-the-art classifiers. We developed a novel method of capturing long-range amino acid dependency conservation by boosting the conservation frequencies of substrings of amino acids of various lengths around the mutation position using AdaBoost learning algorithm. This score alone performed equivalently to the sequence conservation based tools in classifying missense mutations. Popularly used sequence conservation properties was combined with this boosted long-range dependency conservation scores using AdaBoost algorithm. This reduced the class bias, and improved the overall accuracy of the classifer. We trained a third classifier by incorporating changes in 21 important physico-chemical properties, due to the mutation. In this case, we observed that the overall performance further improved and the class bias further reduced. The performance of our final classifier is comparable with the state-of-the-art classifiers. We did not find any significant improvement, but the class-specific accuracies and precisions are marginally better by around 1-2% than those of the existing classifiers. In order to understand our classifier better, we dissected our benchmark dataset into: (a) seen and unseen proteins, and (b) pure and mixed proteins, and analyzed the performance in detail. Finally we concluded that our classifier performs consistently across each of these categories of seen, unseen, pure and mixed protein.

Video Archive Go Top

 

Series: Ph.D. Thesis Defense
Title: Concurrency Analysis and Mining Techniques for APIs

  • Speaker: Mr. Anirudh Santhiar
                   Ph.D student
                   Dept. of CSA
  • Faculty Advisor: Prof. Aditya S Kanade
  • Date and Time: Friday, December 22, 2017, 10:30 AM
  • Venue: CSA Faculty Room, (Room No. 101, Ground floor)

Abstract
Software components expose Application Programming Interfaces (APIs) as a means to access their functionality, and facilitate reuse. Developers use APIs supplied by programming languages to access the core data structures and algorithms that are part of the language framework. They use the APIs of third-party libraries for specialized tasks. Thus, APIs play a central role in mediating a developer’s interaction with software, and the interaction between different software components. However, APIs are often large, complex and hard to navigate. They may have hundreds of classes and methods, with incomplete or obsolete documentation. They may encapsulate concurrency behaviour that the developer is unaware of. Finding the right functionality in a large API, using APIs correctly, and maintaining software that uses a constantly evolving API are challenges that every developer runs into. In this thesis, we design automated techniques to address two problems pertaining to APIs (1) Concurrency analysis of APIs, and (2) API mining. Specifically, we consider the concurrency analysis of asynchronous APIs, and mining of math APIs to infer the functional behaviour of API methods.

The problem of concurrency bugs such as race conditions and deadlocks has been well studied for multi-threaded programs. However, developers have been eschewing a pure multithreaded programming model in favour of asynchronous programming models supported by asynchronous APIs. Asynchronous programs and multi-threaded programs have different semantics, due to which existing techniques to analyze the latter cannot detect bugs present in programs that use asynchronous APIs. This thesis addresses the problem of concurrency analysis of programs that use asynchronous APIs in an end-to-end fashion. We give operational semantics for important classes of asynchronous and event-driven systems. The semantics are designed by carefully studying real software and serve to clarify subtleties in scheduling. We use the semantics to inform the design of novel algorithms to find races and deadlocks. We implement the algorithms in tools, and show their effectiveness by finding serious bugs in popular open-source software.

To begin with, we consider APIs for asynchronous event-driven systems supporting programmatic event loops. Here, event handlers can spin event loops programmatically in addition to the runtime’s default event loop. This concurrency idiom is supported by important

classes of APIs including GUI, web browser, and OS APIs. Programs that use these APIs are prone to interference between a handler that is spinning an event loop and another handler that runs inside the loop. We present the first happens-before based race detection technique for such programs. Next, we consider the asynchronous programming model of modern languages like C#. In spite of providing primitives for the disciplined use of asynchrony, C# programs can deadlock because of incorrect use of blocking APIs along with non-blocking (asynchronous) APIs. We present the first deadlock detection technique for asynchronous C# programs. We formulate necessary conditions for deadlock using a novel program representation that represents procedures and continuations, control flow between them and the threads on which they may be scheduled. We design a static analysis to construct the program representation and use it to identify deadlocks. Our ideas have resulted in research tools with practical impact. SparseRacer, our tool to detect races, found 13 previously unknown use-after-free bugs in KDE Linux applications. DeadWait, our deadlock detector, found 43 previously unknown deadlocks in asynchronous C# libraries. Developers have fixed 43 of these races and deadlocks, indicating that our techniques are useful in practice to detect bugs that developers consider worth fixing.

Using large APIs effectively entails finding the right functionality and calling the methods that implement it correctly, possibly composing many API elements. Automatically inferring the information required to do this is a challenge that has attracted the attention of the research community. In response, the community has introduced many techniques to mine APIs and produce information ranging from usage examples and patterns, to protocols governing the API method calling sequences. We show how to mine unit tests to match API methods to their functional behaviour, for the specific but important class of math APIs.

Math APIs are at the heart of many application domains ranging from machine learning to scientific computations, and are supplied by many competing libraries. In contrast to obtaining usage examples or identifying correct call sequences, the challenge in this domain is to infer API methods required to perform a particular mathematical computation, and to compose them correctly. We let developers specify mathematical computations naturally, as a math expression in the notation of interpreted languages (such as Matlab). Our unit test mining technique maps subexpressions to math API methods such that the method’s functional behaviour matches the subexpression’s executable semantics, as defined by the interpreter. We apply our technique, called MathFinder, to math API discovery and migration, and validate it in a user study. Developers who used MathFinder finished their programming tasks twice as fast as their counterparts who used the usual techniques like web and code search, and IDE code completion. We also demonstrate the use of MathFinder to assist in the migration of Weka, a popular machine learning library, to a different linear algebra library.

Video Archive Go Top

 

Series: CSA Distinguished Lecture
Title: Planar Graph Perfect Matching is in NC

  • Speaker: Professor Vijay Vazirani
                   University of California
                   Irvine
                   USA
  • Date and Time: Thursday, December 21, 2017, 4:00 PM
  • Venue: CSA Seminar Hall (Room No. 254, First Floor)

Abstract
Is matching in NC, i.e., is there a deterministic fast parallel algorithm for it? This has been an outstanding open question in TCS for over three decades, ever since the discovery of Random NC matching algorithms. Within this question, the case of planar graphs has remained an enigma: On the one hand, counting the number of perfect matchings is far harder than finding one (the former is #P-complete and the latter is in P), and on the other, for planar graphs, counting has long been known to be in NC whereas finding one has resisted a solution!

The case of bipartite planar graphs was solved by Miller and Naor in 1989 via a flow-based algorithm. In 2000, Mahajan and Varadarajan gave an elegant way of using counting matchings to finding one, hence giving a different NC algorithm.

However, non-bipartite planar graphs still didn't yield: the stumbling block being odd tight cuts. Interestingly enough, these are also a key to the solution: a balanced odd tight cut leads to a straight-forward divide and conquer NC algorithm. The remaining task is to find such a cut in NC. This requires several algorithmic ideas, such as finding a point in the interior of the minimum weight face of the perfect matching polytope and uncrossing odd tight cuts. Joint work with Nima Anari.

Speaker Bio:
Dr. Vazirani is distinguished professor of computer science in the Donald Bren School of Information and Computer Sciences at the University of California, Irvine. He is a leading researcher in algorithm design, and more generally, in the theory of computing. Throughout his research career, he has demonstrated a consistent ability to obtain novel algorithmic ideas, frequently of substantial mathematical depth, which while solving the problem at hand, also lay the groundwork for future contributions by others. Dr. Vazirani's research career spans over twenty five years. During the first ten years, he made seminal contributions to the classical maximum matching problem which has historically played a central role in the development of the theory of algorithms. He discovered, jointly with other researchers, the fastest known sequential and parallel algorithms for his problem. Over the next ten years, Vazirani focused on approximation algorithms for NP-hard problems and had much influence on this area through work on several of its fundamental problems. In 2001, he published a book on this topic. He is currently working in algorithmic game theory, in particular on algorithms for computing market equilibria.

Host Faculty: Dr. Siddharth Barman

Video Archive Go Top

 

 

 

 

 

 

 

 

 

 

Copyright: CSA, IISc 2017      Phone: +91-80-22932368          Fax: +91-80-23602911 Travel Blog    Feedback    Credits