Appears in collection : 19th International Conference on Relational and Algebraic Methods in Computer Science / 19ème Conférence internationale de méthodes relationnelles et algébriques en informatique
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.
By Anne Driemel
By Anna Korba
