Abstract: Researchers have rightfully been concerned about preventing memory errors, but in doing so have ignored methods to improve the security of the parts of the program that are already memory safe. We propose techniques to perform comprehensive memory safety validation that identify the program objects whose accesses…

Abstract: Binary decision diagrams (BDDs) are directed acyclic graphs used to represent functions over boolean variables. They have enjoyed widespread success in a number of domains, including hardware verification, model checking, and combinatorial problems. This talk presents RexBDDs, a form of BDDs that can exploit…