The TAU Programming Languages and Systems Seminar - A context-sensitive memory model for software model checking

Abstract:

Model-Checking of low-level C and C++ requires a precise memory model

that supports type unions, pointer arithmetic, and casts. In this

talk, I will present our work on a new memory model that splits memory

into a finite set of disjoint regions based on a pointer analysis. Our

main contribution is a field-, array- and context-sensitive pointer

analysis tailored to verification. We have integrated the memory model

and the corresponding alias analysis into our software model checker

SeaHorn. The new memory model is shown to be effective on a case study

of verifying memory safety of a C++ program as well as on SV-COMP

verification benchmarks. Our results suggests that our model reduces

verification time by producing a finer-grained partitioning in

presence of function calls than other, non-context-sensitive memory

models, commonly used by software model checkers today.

Bio:

Arie Gurfinkel holds a Ph.D. in Computer Science from the Computer

Science Department of University of Toronto (2007). He is an Associate

Professor at the Department of Electrical and Computer Engineering at

the University of Waterloo. Between 2007 and 2016, he was a Principal

Researcher at the Carnegie Mellon Software Engineering Institute. His

research interests lie in the intersection of formal methods and

software engineering, with an emphasis on automated reasoning about

software systems. He has co-lead development of a number of

automated verification tools including the first multi-valued

model-checker XChek, award winning software verification frameworks

UFO and SeaHorn, and a hardware model-checker Avy.