March 28, 2013 (Thursday) CSE Seminar Room (No. 107) 4:30 PM
Bounded Model Checking and HW - SW Co-verification
Dr. M. K. Srivas
Computer Science Department
Chennai Mathematical Institute
Bounded Model Checking (BMC) has seen significant growth in recent past in application to industrial-scale mixed control and data-dominated HW/SW designs. A main reason behind this are the recent advances in SAT (Boolean-satisfiability) and SMT (Satisfiability-Modulo-Theories), two important back-end technologies used in several FV tools, have had a dramatic positive impact on scalability. A major attraction of BMC is its range of applicability: from specification level (e.g., statecharts) to high-level models (C/C++) to actual code (C, Verilog/VHDL). In this series of presentations (to be given as part of Pallab Dasgupta's Course lectures), I will give a detailed description of SAT solving, an overview of BMC for mixed C and Verilog models. I will then illustrate a few examples on the BMC tool HW-CBMC from Oxford University.
Dr. M. K. Srivas is on the faculty of Computer Science Department at Chennai Mathematical Institute and a Visiting Professor at Oxford University, Oxford, UK. Srivas got his Masters from IISc, Bangalore, and PhD from MIT, USA, and has more than 25 years of academic and industrial experience in formal verification (FV). After serving on the faculty of CS Dept. at State University of Stony Brook, USA, he was an R&D scientist at SRI, International, CA. At SRI, Srivas pioneered application FV for commercial microprocessor designs. He was a Director of a VLSI start-up company, Nulife Semiconductor, India, which specialized in low-power mixed-signal ASIC design for hearing-aid application. Nulife was later merged with Texas Instruments, India, where Srivas was Senior Member of Technical staff and General Manager. His main research interests are in high-level modeling and formal verification of embedded systems. He has hands-on experience of having developed and applied formal methods for assuring safety and integrity of embedded systems for IP in an industrial setting. He has delivered tutorial lectures on FV for industrial audiences (Rockwell International and TI) and at Arhus Summer School on verification, Aarhus University, Denmark, 1998. He started the Formal Methods in CAD (FMCAD) conference (now a premier conference in FV) and has served on the PC of several conferences (CAV, FMCAD, ICCAD).
February 18, 2013 (Monday) CSE Seminar Room (No. 107) 3:00 PM
Annotating Images with Words, Phrases and Sentences
Prof. C. V. Jawahar
In this talk, we present some of our recent attempts on tagging visual data with textual descriptions.
Automatic Annotation process learns to predict the tags from examples.
Tags could be a set of words, phrases or even sentences.
Our method uses simple machine learning and optimization schemes for annotating images and videos.
Our method outperforms the state of the art methods which uses more complex models for related tasks.
Our method captures the prior and statistics of the textual data, and uses it in a nearest neighbour setting with learned distance measures.
Parts of this work appeared in AAAI 2012 and ECCV 2012.
C. V. Jawahar received his PhD from IIT Kharagpur in 1997. After that, he worked for Center for AI and Robotics, Bangalore till 2000. He joined IIIT Hyderabad in 2000 to initiate a research group focusing on visual information processing. He is presently a Professor at IIIT Hyderabad, and heads the Center for Visual Information Technology. His research interests span the broad areas of Computer Vision, Machine Learning and Multimedia Systems.
February 13, 2013 (Wednesday) CSE Seminar Room (No. 302) 9:30 AM
Automation in process industry and Computer Science in Automation
with an interesting example
Dr. Arya Bhattacharya
This talk will provide an introduction to the basics of the steel making process and will dwell on the role of Automation. It will then discuss on the technical content of Automation generically and the role of Computer Science & IT, and identify disciplines within Computer Science that contribute to the state-of-art in Automation. Finally it will discuss one interesting example of application of data mining to continuous-time systems in process industry.
January 30, 2013 (Wednesday) CSE Seminar Room (No. 107) 3:30 PM
Block Cipher Modes for Disk Encryption
Security of data stored in bulk storage devices like hard disks, flash memories etc. has gained a lot of importance in the current days. In this talk we shall discuss cryptographic techniques which can be applied for encrypting data stored in storage devices like hard disks. We shall focus on a class of schemes called tweakable enciphering schemes (TES) which are known to be suitable for the application. The general syntax and security of TES would be discussed.
Finally we would talk about some specific constructions of TES along with their security characteristics and implementational issues.
Debrup Chakraborty received the BE degree in mechanical engineering from Jadavpur University, Kolkata, India, in 1997, and the MTech and PhD degrees in computer science from the Indian Statistical Institute, Kolkata, in 1999 and 2005, respectively. Currently, he is a senior researcher in the Computer Science Department of Centro de Investigaciones y Estudios Avanzados del IPN (CINVESTAV-IPN), Mexico City, Mexico.
His current research interests includes design and analysis of provably secure symmetric encryption schemes and efficient software/hardware implementations of cryptographic algorithms.
January 3, 2013 (Thursday) CSE Seminar Room (No. 107) 3:30 PM
Breaking the barrier for low-power and energy-efficiency:
An Adaptive and Self-Healing Approach
Dr. Swaroop Ghosh
University of South Florida
Achieving low-power and energy-efficiency in order to maintain the reliability of the VLSI systems is becoming challenging in scaled technologies. The energy dissipation per computation is limited by the lowest operating supply voltage (Vmin). In state of the art design, failures due to process variation obstruct the Vmin scaling. In this talk, I will present some of the disruptive design principles in logic and memories to break the Vmin wall and attain highly energy-efficient nanoscaled systems. In particular, I will discuss an adaptive and self-healing design philosophy for logic to lower the Vmin without sacrificing frequency or functionality. Next, I will present self-healing embedded memories to lower the Vmin without any functional failures. The ultimate aim is to develop low-power, energy-efficient and self-healing systems that would function even under process uncertainties.
Dr. Swaroop Ghosh received his B.E. (Hons.) from Indian Institute of Technology, Roorkee, India in 2000 and Ph.D. from Purdue University in 2008. He joined the faculty of University of South Florida in Fall 2012. Dr. Ghosh was a senior research and development engineer in Advanced Design, Intel Corp from 2008 to 2012. At Intel, his research was focused on low power and robust embedded memory design in scaled technologies. He has filed four US patents, published over 30 papers and authored a book chapter. He has served in the technical program committees of VLSI Design, ISQED, ASQED, VLSI-SOC, IEDEC and NDCS. His research interests include low-power, energy-efficient and robust circuit/system design and digital testing for nanometer technologies. Dr. Ghosh is a member of IEEE.
January 3, 2013 (Thursday) CSE Seminar Room (No. 107) 11 AM
ARM Architecture Fundamentals
ARM products are commonly used in billions of electronic systems like smartphones, hard disk drives, digital televisions, set-top boxes and microcontrollers. The primary purpose of this ARM University talk is to create awareness about ARM processors among engineering students. This presentation highlights the basics of the ARM instruction set architecture. The talk commences with an introduction to ARM, its history, activities and some basic applications of ARM processors. The presentation provides an overview of the ARM ISA, the programmers view, and the basic instruction types. The evolution of ARM microarchitecture is explained as well. Next, some illustrated examples of ARM based systems are presented. An introduction to ARM University, its activities and services will conclude the talk. This presentation will be of significance to undergraduate students in computer science, electronics and electrical engineering departments who are interested in computer organization and embedded systems.
ARM Microarchitecture Basics:
ARM products are used in billions of electronic systems like smartphones, hard disk drives, digital televisions, set-top boxes and microcontrollers. The primary purpose of this talk is to create awareness about ARM processors among engineering students. This presentation highlights the microarchitecture of a contemporary ARM processor. The talk commences with an introduction to ARM, its history, activities and some basic applications of ARM processors. The presentation provides a description of the evolution of the ARM microarchitecture. The bulk of the talk will consist of a description of all aspects of the out-of-order pipeline consisting of fetch, rename, issue, execute and commit in context of the Cortex A15 processor. An introduction to ARM University, its activities and services will conclude the talk. This talk will be of significance to senior undergraduate and graduate students in computer science, electronics and electrical engineering departments who are interested in computer organization and advanced computer architecture.
Dr. Mrinmoy Ghosh is a Senior Design Engineer in the Research and Development group at ARM. He has worked at ARM for the last 4 years on system level analysis, prefetchers, and memory hierarchy optimizations. He received his Ph.D. from Georgia Institute of Technology on low power microarchitectural techniques, and his M.S. and B. Tech from the Indian Institute of Technology, Kharagpur.
2012 | 2011 | 2010 | 2009 | 2008