TCS Interaction Day

September 7-8, 2015

September 7, 2015 Venue: RM 301
Time Event
0855 Opening
900-1000 Veri-FAST - Towards Zero Defect Software
Shrawan Kumar, TCS Pune Abstract
1000-1100 Domain-driven analytics research in Systems Research Lab, TCS Pune.
Girish Palshikar, TCS, Pune Abstract
1100-1115 Tea Break
1115 -1145 Monoid actions or: How to twist pointers without breaking them.
Piyush Kurur, CSE, IITK Abstract
1145-1215 Safety-Critical Software Synthesis from Polychronous Formal Specification
Sandeep Shukla, CSE, IITK Abstract
1215-1315 PREMAP - A Platform for Integrated Computational Materials Engineering
Sreedhar Reddy, TCS, Pune Abstract
1315-1445 LUNCH BREAK
1445-1545 Modelling the Enterprise - in search of data-driven certainty
Vinay Kulkarni, TCS, Pune Abstract
1545-1615 Tea Break
1615-1715 Multiplicative Weights Optimizer Game Theory: A toolbox for fast and approximate solutions for large linear and semidefinite program
Dilys Thomas, TCS, Pune Abstract
1715-1800 Automated Software Synthesis for Cyber-Physical Systems
Indranil Saha, CSE Abstract
1800-1900 Discussions with IITK faculty

September 8, 2015 Venue: RM 301
Time Event
830-840 Overview of TCS RSP scheme. Sachin Parkhi, RSP team
8:40 - 9:10 Talk by a TCS Scientist + Q&A
Vinay Kulkarni, TCS Chief Scientist, TCS
9:10 - 9:40 Brief overview of research supported by TCS RSP + Q&A  
      Talk by TCS Research  Scholar - Naveen Kumar
9.40 – 10.10 Liveness-Based Garbage Collection
Amey Karkare, CSE IITK Abstract
10:10 - 10:40 Overview of Recent Technological Applications + Q&A Shashi Bhushan - Chief Evangelist, TCS
10:40 - 11:10 Open House with students and Faculty – opportunities galore Haridas Menon - Head -CTO HR, TCS
11:10-11:30 Tea

Abstract : Veri-FAST - Towards Zero Defect Software

Shrawan Kumar, Senior Scientist, Tata Consultancy Services, Pune

Abstract

This talk will give brief details of problems and research areas in which our group 'Verif-FAST' has been working. The broad areas are static analysis, model checking, specification and Testing. Focus is on achieving highly scalable solutions with a very low false positive rate. We have come up with some unique patterns to be detected through analysis which help in detecting domain specific defects in embedded software. We have developed some new techniques like LABMC and value slice which enable high degree of precision with no loss in scalability. In specification, we have devised an easy to use language to specify reactive systems. The specification themselves are analysed to detect inconsistencies and missing requirements. We use the same specifications to generate test cases which guarantee 100% coverage of requirements. Focus is to achieve higher coverage with lesser efforts.

Abstract: Domain-driven analytics research in Systems Research Lab, TCS Pune.

Girish Keshav Palshikar, Senior Scientist, Tata Consultancy Services, Pune.

Abstract

In this talk, we shall review the various research work done in Systems Research Lab, TCS Pune, with a focus on the domains of Human Resource Management and Fraud Detection.

Abstract: Monoid actions or: How to twist pointers without breaking them.

Prof. Piyush Kurur, CSE, IIT Kanpur

Abstract

In this talk, we show how certain pointer manipulation tasks can be abstracted and refactored out using *monoid actions*, i.e. monoids together with an action on some type/set. We start with the semi-direct product of two monoids and show how this construct can capture data serialisation. The semi-direct product construction can be generalised to what we call *twisted functors* which form the basis of many common tasks involving pointer manipulations like packet parsing, memory allocation etc. Source code at: https://github.com/raaz-crypto/raaz . Joint work with: Satvik Chauhan

Abstract: Safety-Critical Software Synthesis from Polychronous Formal Specification

Prof. Sandeep Shukla, CSE, IIT Kanpur

Abstract

In this talk we will talk about our embedded software synthesis tool 'EmCodeSyn' which synthesizes reactive software through a 'correct-by-construction' methodology. The specification language MRICDR is a polychromous language with a graphical and textual front-end. The methodology consists of clock analysis and data-flow analysis aided by SMT solvers which characterizes the specification as endochronous, weakly endochronous or exochronous. Based on the characterization, sequential, multi-threaded or externally controlled software are generated. The generation process is a refinement technique that preserves temporal properties, and thereby guaranteeing the correctness with respect to the specification. We will also discuss methods for proving correctness of the specification as without correct specification, a 'correct-by-construction' would not provide correctness guarantees. We shall also briefly discuss our plans on building a center for security of critical infrastructure at IITK at the end of the talk.

Abstract: PREMAP - A Platform for Integrated Computational Materials Engineering

Sreedhar Reddy, Chief Scientist, Tata Consultancy Services, Pune, India

Abstract

Integrated computational materials engineering (ICME) is a new approach to the design and development of materials, manufacturing processes and products. The approach proposes using a combination of modeling and simulation, data driven reasoning and knowledge guided decision making to a) speed up the development of new materials and manufacturing processes, and b) enhance the quality and time-to-market of products by integrating material design with product design. We discuss the challenges involved in building a computational platform to support this approach and our solutions to some of these challenges.

Abstract: Modelling the Enterprise - in search of data-driven certainty

Vinay Kulkarni, Chief Scientist, Tata Consultancy Services, Pune, India

Abstract

The modern enterprise is a complex socio-technical system operating in a dynamic environment. It needs to respond quickly to the several change drivers maintaining key strategic, operational and regulatory parameters. Size and complexity of modern enterprise means the cost of erroneous response is high, and there is rarely an opportunity for later course correction. The current practice which relies heavily on experts interpreting information captured in document form, is turning out to be ineffective. Modeling and simulation have served well to impart agility as well as a priori certainty, but only in situations where the mechanistic world view holds. We are exploring how they can be made to deliver equally well in socio-technical context.

Abstract: Multiplicative Weights Optimizer Game Theory: A toolbox for fast and approximate solutions for Large Linear and Semidefinite programs

Dilys Thomas, Tata Consultancy Services, Pune, India

Abstract

The multiplicative weights update is an algorithmic design technique that, over the years, has been discovered independently by several groups of researchers in different contexts. The earliest known use of this techniqueis by Brown and von Neumann for the computation of equilibrium strategies in zero-sum games. These ideas and variants thereof have found applications in solving games, linear and semidefinite programming, computational geometry, machine learning, auctions and mechanism design, as well as data privacy. In this work, we focus on the use of this technique for solving zero-sum games, and for solving linear and semidefinite programs. In particular, we present empirical results on the efficacy of this method to solve linear and semidefinite programs approximately. Our results suggest that this could be the preferred method in scenarios where one is interested in obtaining reasonably good results very quickly, as well as in scenarios where the problem sizes are very large. Another advantage of this technique is that it is amenable to a parallel or distributed implementation unlike interior point or simplex methods, and therefore could form a primitive in cluster computing, or in sensor networks.

Title: Automated Software Synthesis for Cyber-Physical Systems

Indranil Saha, CSE, IIT Kanpur

Abstract

Embedded and cyber-physical systems are used in numerous mission-critical and life-critical applications. Most of these systems run sophisticated control algorithms at their core in the form of embedded software. The development flow of such software has two major steps: (1) mission planning from high level specification that generates a sequence of tasks to be executed by the system, and (2) synthesis of a set of feedback controllers in the form of embedded software that regulate the system to perform the tasks. In this talk, I will describe how automated software synthesis techniques can be useful in implementing these steps in developing high-assurance embedded control software. First, I will describe how one can synthesize the trajectories for a group of robots to satisfy their​ high-level mission specification by composing their motion primitives using an SMT solver. Second, I will describe how one can synthesize optimal performance software for the feedback controllers that regulate the robots to follow the motion primitives. I will conclude the talk by outlining future research directions in the area of automated synthesis of software for robotic applications.

Title: Liveness-Based Garbage Collection

Amey Karkare, CSE, IIT Kanpur

Work done with Prasanna K (IITB), Rahul Asati (IITB), Amitabha Sanyal (IITB), and Alan Mycroft(University of Cambridge).

Abstract

Current garbage collectors leave much heap-allocated data uncollected because they preserve data reachable from a root set. However, only live data—a subset of reachable data—need be preserved. We formulate a context-sensitive liveness analysis for structured data and prove it correct. We then use a 0-CFA-like conservative approximation to annotate each allocation and function-call program point with a finite-state automaton—which the garbage collector inspects to curtail reachability during marking. As a result, fewer objects are marked (albeit with a more expensive marker) and then preserved (e.g. by a copy phase). Experiments confirm the expected performance benefits—increase in garbage reclaimed and a consequent decrease in the number of collections, a decrease in the memory size required to run programs, and reduced overall garbage collection time for a majority of programs.