Relational tight field bounds for distributed analysis of programs
Relational tight field bounds are an abstraction of the semantics of data structures. In the presence of appropriate symmetry-breaking predicates, these bounds can be computed automatically and allow to dramatically speed up bug-finding using SAT- solving. In this lecture, after giving an introduction to tight field bounds and symmetry- breaking predicates, I will present a general technique for distributing program analyses. As examples, I will show how the technique allows one to distribute SAT-based bug-finding as well as symbolic execution over complex data types.