Symbolic Abstraction with SMT Solvers

Yi Li

University of Toronto, 2013

Abstract: Numerical invariant generation is an important program analysis task with uses spanning compiler optimizations, bug finding, and verification. Abstract interpretation with numerical domains is one of the most scalable automated techniques for computing numerical invariants. Unfortunately, efficiency is often achieved by employing imprecise operations (e.g., join and abstract post). Moreover, expressive domains such as polyhedra are expensive, and efficient domains such as intervals are often too weak to prove interesting program properties. In this thesis, we present Symba, a novel algorithm that harnesses the power and precision of SMT solvers, in order to (1) implement precise (best) abstract transformers over large program segments described as formulas in linear real arithmetic (QF_LRA), thus avoiding the imprecision incurred by abstract post computations over single instructions or basic blocks; (2) avoid the use of imprecise join operations by symbolically and efficiently enumerating program paths; and (3) enable invariant generation in the Template Constraint Matrix (TCM) domain, a parameterized domain that subsumes intervals, octagons, and octahedra, amongst other domains.

Cite:

@mastersthesis{Li2013SAS,
  author = {Li, Yi},
  month = jan,
  school = {University of Toronto},
  title = {Symbolic Abstraction with {SMT} Solvers},
  year = {2013}
}