Formal Methods in an Informal World


Prof. Dr. Pallab Dasgupta

25.06.2015, 16:00, room 4981


The use of formal methods has been recommended in various industrial safety standards, including Aeronautics (DO-178C), Automotive (ISO 26262), Industrial process automation (IEC 61508), Nuclear (IEC 60880), Railway (EN 50128), Space (ECSS-Q-ST-80C). It is in general far from clear how these recommendations are to be interpreted and what it means to formally certify a design to be correct. Formalisms for expressing the design intent are being introduced in various domains with various degrees of rigour, but the major irritant is in formally interpreting the world in which the design is expected to work correctly. This talk intends to provide a brief exposition of the challenges in using formal methods in a world without adequate formalization, focussing on techniques from automated verification, abstraction refinement and counter-example ranking.


Dr. Pallab Dasgupta is a computer scientist known for his work on formal methods for design automation of electronic circuits and systems. He is currently a professor with the department of Computer Science and Engineering at IIT Kharagpur, which gives him the license to teach some of the great young minds of India, collaborate with many companies who come to him with very tough problems, and provide research guidance to some students who are reasonably determined to get their PhD degrees. He plays, though not very well, an Indian instrument called sitar. He has recently started collaborating with musicians, computer scientists, signal processing engineers and psychologists to discover the SANDHI (or amalgamation) of technology and music. He is a Fellow of the Indian National Academy of Engineering and a Fellow of the Indian Academy of Sciences. Other not so relevant information about him can be found in his website: