Login
Talks & Seminars
Title: Underspecified Harnesses and Interleaved Bugs
Dr. Shuvendu Lahiri, Microsoft Research, Redmond
Date & Time: December 8, 2011 15:00
Venue: SIC301, 03rd floor, C Block, Dept. of CSE, Kanwal Rekhi Bldg.
Abstract:
Static assertion checking of open programs requires setting up a precise harness to capture the environment assumptions. For instance, a library may require a file handle to be properly initialized before it is passed into it. A harness is used to set up or specify the appropriate preconditions before invoking methods from the program. In the absence of a precise harness, even the most precise automated static checkers are bound to report numerous false alarms. This often limits the adoption of static assertion checking in the hands of a user. In this work, we explore the possibility of automatically filtering away (or prioritizing) warnings that result from imprecision in the harness. We limit our attention to the scenario when one is interested in finding bugs due to concurrency. We define a warning to be an interleaved bug when it manifests on an input for which no sequential interleaving produces a warning. As we argue in the paper, limiting a static analysis to only consider interleaved bugs greatly reduces false positives during static concurrency analysis in the presence of an imprecise harness. We formalize interleaved bugs as a differential analysis between the original program and its sequential version and provide various techniques for finding them. Our implementation CBugs demonstrates that the scheme of finding interleaved bugs can alleviate the need to construct precise harnesses while checking real-life concurrent programs. Joint work with Saurabh Joshi (IIT Kanpur) and Akash Lal (MSR India). Will be presented at POPL'12.
Speaker Profile:
Dr. Shuvendu Lahiri is a researcher in the Research in Software Engineering (RiSE) group at Microsoft Research, Redmond. His research focuses on program verification, symbolic methods and theorem proving. He has worked on verifying heap manipulating C programs, modeling and verifying unbounded systems, predicate abstraction methods and SMT solvers. More recently, he has been applying program verification ideas for differential program analysis. He obtained a PhD from Carnegie Mellon University and a BTech from Indian Institute of Technology, Kharagpur. His PhD thesis received the ACM SIGDA Outstanding Thesis Award for the year 2004-2005. More information can be found at http://research.microsoft.com/en-us/people/shuvendu/.
List of Talks

Webmail

Username:
Password:
Faculty CSE IT
Forgot Password
    [+] Sitemap     Feedback