Inferring polynomial invariants with Polyinvar
Helmut Seidl, Michael Petter · 2005
Model Polynomial programs... • modelling control flow with (possibly annotated) edges • assignments of multivariate polynomial expressions (without division) x := y · y + x • method calls x := f (y , z) • unknown assignments x :=? ... with guards • negative polynomial equality guards (y − n) 6= 0 • positive polynomial equality guards (y − n) = 0 • non deterministic choice for the rest skip → Goal: inferring all valid polynomial relations Motivation Model Intraprocedural analysis Interprocedural analysis Conclusion Abstract Model Polynomial programs... • modelling control flow with (possibly annotated) edges • assignments of multivariate polynomial expressions (without division) x := y · y + x • method calls x := f (y , z) • unknown assignments x :=? ... with guards • negative polynomial equality guards (y − n) 6= 0 • positive polynomial equality guards (y − n) = 0 • non deterministic choice for the rest skip → Goal: inferring all valid polynomial relationsModel Polynomial programs... • modelling control flow with (possibly annotated) edges • assignments of multivariate polynomial expressions (without division) x := y · y + x • method calls x := f (y , z) • unknown assignments x :=? ... with guards • negative polynomial equality guards (y − n) 6= 0 • positive polynomial equality guards (y − n) = 0 • non deterministic choice for the rest skip → Goal: inferring all valid polynomial relations Motivation Model Intraprocedural analysis Interprocedural analysis Conclusion Abstract Model Polynomial programs... • modelling control flow with (possibly annotated) edges • assignments of multivariate polynomial expressions (without division) x := y · y + x • method calls x := f (y , z) • unknown assignments x :=? ... with guards • negative polynomial equality guards (y − n) 6= 0 • positive polynomial equality guards (y − n) = 0 • non deterministic choice for the rest skip → Goal: inferring all valid polynomial relationsModel Polynomial programs... • modelling control flow with (possibly annotated) edges • assignments of multivariate polynomial expressions (without division) x := y · y + x • method calls x := f (y , z) • unknown assignments x :=? ... with guards • negative polynomial equality guards (y − n) 6= 0 • positive polynomial equality guards (y − n) = 0 • non deterministic choice for the rest skip → Goal: inferring all valid polynomial relations Motivation Model Intraprocedural analysis Interprocedural analysis Conclusion Abstract Model Polynomial programs... • modelling control flow with (possibly annotated) edges • assignments of multivariate polynomial expressions (without division) x := y · y + x • method calls x := f (y , z) • unknown assignments x :=? ... with guards • negative polynomial equality guards (y − n) 6= 0 • positive polynomial equality guards (y − n) = 0 • non deterministic choice for the rest skip → Goal: inferring all valid polynomial relationsModel Polynomial programs... • modelling control flow with (possibly annotated) edges • assignments of multivariate polynomial expressions (without division) x := y · y + x • method calls x := f (y , z) • unknown assignments x :=? ... with guards • negative polynomial equality guards (y − n) 6= 0 • positive polynomial equality guards (y − n) = 0 • non deterministic choice for the rest skip → Goal: inferring all valid polynomial relations Motivation Model Intraprocedural analysis Interprocedural analysis Conclusion Intraprocedural example squarepowsum (n ∈ N) ∈ N { x, y ∈ N; x ⇐ 0, y ⇐ 0; while (y 6= n){ y ⇐ y + 1; x ⇐ y · y + x; } return x; } State abstraction Still, we have to find an abstraction for program states that serves our analysis... y := y + 1 skip (y − n 6= 0)