Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis

Assalé Adjé, Stéphane Gaubert, Eric Goubault

We introduce a new domain for finding precise numerical invariants of programs by abstract interpretation. This domain, which consists of level sets of non-linear functions, genera…