| Title | : | The Science of Correct-by-Construction Programming |
| Speaker | : | Om Damani (Dept of CSE, IIT Bombay, India) |
| Details | : | Fri, 6 Nov, 2015 12:00 PM @ BSB 361 |
| Abstract: | : | Software Engineers often rely on testing to gain confidence that the
implemented programs are defect-free. Formal verification tools are
also employed in few select domains where errors have greater
significance. However, since testing/verification is done after the
system has been implemented; it does not provide any help to the
programmer during the implementation phase. In contrast with this, in the Calculational Style of Programming, programs are incrementally derived from their specifications. At every step in the derivation process, a partial program is transformed into a more refined form, by following certain transformation rules. The resulting programs are correct-by-construction since the correctness is implicit in the program transformations employed during the derivation. By calculation, we mean that program constructs are introduced only when logical manipulations show them to be sufficient for correctness based on their pre- and post- conditions. Despite resulting in simple and elegant programs, the Calculational style did not become popular due to the various practical difficulties that prevented wider adoption of this methodology. Even for small programming problems, the derivations are often long and difficult to organize. As a result, the derivations, if done manually, are error-prone and cumbersome. To address these issues, we have built an IDE called CAPS (Calculational Assistant for Programming from Specifications). CAPS has built-in refinement rules and the system generates the required correctness proof obligations. In building CAPS, our aim has been to make the IDE accessible to nonexperts while retaining the overall flavor of the pen-and-paper style derivation. Speaker Bio: Dr. Om Damani received the B. Tech. degree in Computer Science and Engineering, IIT Kanpur in 1994 and Ph.D. degree in Computer Sciences from the University of Texas at Austin in 1999. Post-PhD, he has worked at Akamai Technologies Inc., Cambridge, USA and IBM TJ Watson Research Lab, USA. Since 2004, he has been a faculty member at IIT Bombay. He has received the IIT Bombay Industrial Impact Award 2010, along with Prof. Umesh Bellur and Prof. D. B. Phatak, for their consultancy work on Designing a New Mission-Critical Depository System for National Securities Depository Limited (NSDL), Mumbai. Host: Prof. Krishna Moorthy Sivalingam, Professor, CSE Dept, IIT Madras, Chennai, India |
