Colloquium
Shuvendu Lahiri
Microsoft Research
Monday, April 29, 2013
3147 MEB
Refreshments 3:20 p.m.
Lecture 3:40 p.m.
Title: Making program verifiers less demonic by exploiting the specifications within
Shuvendu Lahiri
Microsoft Research
Monday, April 29, 2013
3147 MEB
Refreshments 3:20 p.m.
Lecture 3:40 p.m.
Title: Making program verifiers less demonic by exploiting the specifications within
Abstract
Program verifiers (in particular assertion checkers) have made tremendous progress over the last several years. However, the demonic nature of program verifiers preclude them from being adapted by average developers, due to the need for substantial domain-specific modeling before obtaining value from such a tool. The modeling comes in the form of providing extensive environment specifications and providing internal invariants that are beyond the invariant inference. The absence of precise modeling leads to program verifiers generating numerous "stupid" errors, that are a strong deterrent to initial adoption of sophisticated program verifiers. Unfortunately, the area of making program verifiers less demonic, or alternately trading off soundness for precision using systematic techniques, is understudied.
In this talk, I will describe some directions to make program verifiers more friendly by respecting the contracts implicit in the code. I will present two main concepts (a) differential assertion checking (DAC), and (b) almost-correct specifications. Differential assertion checking aims at trading off soundness by providing relative guarantees of correctness instead of absolute correctness. I will discuss applications of DAC towards checking assertions in concurrent programs (POPL'12) and towards exploiting previous versions of a program. The framework of almost correct specifications (PLDI'13) provides a framework for prioritizing alarms modularly by exploring the space between the angelic and demonic specifications for a program.
BIO
Dr. Shuvendu Lahiri is a researcher in the Research in Software Engineering (RiSE) team at Microsoft Research, Redmond. He is interested in symbolic methods for improving the analysis of software. His current focus lies in using symbolic methods to perform differential static analysis and semantic methods to prioritize warnings from program verifiers. He has worked on logics and decision procedures, algorithms for dealing with heap-manipulating programs, abstraction techniques for hardware and software. Shuvendu holds a PhD in Computer Engineering from Carnegie Mellon University and a BTech from IIT Kharagpur. His PhD dissertation on indexed predicate abstraction received the ACM SIGDA outstanding thesis award for 2005. More information can be found at here
Program verifiers (in particular assertion checkers) have made tremendous progress over the last several years. However, the demonic nature of program verifiers preclude them from being adapted by average developers, due to the need for substantial domain-specific modeling before obtaining value from such a tool. The modeling comes in the form of providing extensive environment specifications and providing internal invariants that are beyond the invariant inference. The absence of precise modeling leads to program verifiers generating numerous "stupid" errors, that are a strong deterrent to initial adoption of sophisticated program verifiers. Unfortunately, the area of making program verifiers less demonic, or alternately trading off soundness for precision using systematic techniques, is understudied.
In this talk, I will describe some directions to make program verifiers more friendly by respecting the contracts implicit in the code. I will present two main concepts (a) differential assertion checking (DAC), and (b) almost-correct specifications. Differential assertion checking aims at trading off soundness by providing relative guarantees of correctness instead of absolute correctness. I will discuss applications of DAC towards checking assertions in concurrent programs (POPL'12) and towards exploiting previous versions of a program. The framework of almost correct specifications (PLDI'13) provides a framework for prioritizing alarms modularly by exploring the space between the angelic and demonic specifications for a program.
BIO
Dr. Shuvendu Lahiri is a researcher in the Research in Software Engineering (RiSE) team at Microsoft Research, Redmond. He is interested in symbolic methods for improving the analysis of software. His current focus lies in using symbolic methods to perform differential static analysis and semantic methods to prioritize warnings from program verifiers. He has worked on logics and decision procedures, algorithms for dealing with heap-manipulating programs, abstraction techniques for hardware and software. Shuvendu holds a PhD in Computer Engineering from Carnegie Mellon University and a BTech from IIT Kharagpur. His PhD dissertation on indexed predicate abstraction received the ACM SIGDA outstanding thesis award for 2005. More information can be found at here