Abstract: Predicate (PA) and Numeric (NA) abstractions are the two principal techniques for software analysis. In this talk, we describe an approach to couple the two techniques tightly into a unified framework via a single abstract domain called NumPredDomain. We will describe four data structures that implement NumPredDomain. These data structures differ in their expressivity, internal representation, and algorithms. All of our data structures combine BDDs (for efficient propositional reasoning) with data structures for representing numerical constraints. Our technique is distinguished by its support for complex transfer functions that allow two way interaction between predicate and numeric information during state transformation. We will show how the NumPredDomain is used for reachability analysis of C programs, and describe a set of experiments that illustrate that the combination of PA and NA is more powerful and more efficient than either PA or NA in isolation.

Arie Gurfinkel received a Ph.D., a M.Sc., and a B.Sc. in Computer Science from Computer Science Department of University of Toronto in 2007, 2003, and 2000, respectively. He is currently a Member of Technical Staff at the Software Engineering Institute at Carnegie Mellon University. His research interests lie in the intersection of formal methods and software engineering, with an emphasis on automated techniques for program verification. He was a lead developer for a number of automated verification tools including a multi-valued model-checker XChek, and a software model-checker Yasm. He has more than 28 publications in peer reviewed journals and conferences.

Sagar Chaki Appointments: dcm@cs.cmu.edu