Scaling Systematic Checking Using Incremental and Memoization Techniques

  • Date
    March 27, 2013
  • Time
    2:00pm
  • Location
    366 WVH

Abstract

As software systems become increasingly complex and ubiquitous, the need to develop higher quality software at a lower cost becomes more and more urgent. This talk presents a novel methodology for more efficient and effective checking of programs using systematic techniques. The key insight is that checking a program often requires a number of successive applications of the technique on largely similar underlying problems, e.g., after bug fixes or feature additions to a program, and each subsequent application can leverage the similarities in the successive problems for enhanced efficacy. The talk focuses on symbolic execution, an increasingly popular technique, which poses key technical challenges for scalability. Two novel approaches that embody the insight for scaling symbolic execution are presented. They introduce an incremental method where edits to a program guide its checking and memoization of computations during previous checks reduces the overall cost of checking. Experimental results using a suite of programs, including some from NASA, show the effectiveness of the method in commonly used checking scenarios, such as regression analysis.

Brief Biography

Guowei Yang is completing his Ph.D. in Software Engineering at the Department of Electrical and Computer Engineering in the University of Texas at Austin.  Guowei received a B.E. in Software Engineering from Harbin Institute of Technology, an M.E. in Computer Software and Theory from Institute of Software Chinese Academy of Sciences, and an M.S. in Computer Science from University of Nebraska – Lincoln. His research addresses various elements of how to enhance software reliability and dependability, including software testing and verification, software evolution, symbolic execution, model checking, static and dynamic analysis, and lightweight formal methods. His doctoral research focuses on developing techniques and tools to enable more efficient and effective checking of complex software systems.  As an intern researcher, Guowei worked at Fujitsu Laboratories of America in Fall 2012, NASA Langley Research Center and National Institute of Aerospace in Summer 2012, and NASA Ames Research Center in Summer 2010. He also participated in the Google Summer of Code with the Java PathFinder (JPF) Team in Summer 2011.