1: \begin{abstract}

2: % PERFEKT

3: We consider the problem of computing numerical invariants of programs by abstract interpretation.

4: Our method eschews two traditional sources of imprecision:

5: (i) the use of widening operators for enforcing convergence within

6: a finite number of iterations (ii) the use of merge operations (often,

7: convex hulls) at the merge points of the control flow graph. It instead

8: computes the least inductive invariant expressible in the domain

9: at a restricted set of program points, and analyzes the rest of the code en bloc. 

10: We emphasize that we compute this inductive invariant precisely.

11: For that 

12: we extend the strategy improvement algorithm of \citet{DBLP:conf/csl/GawlitzaS07}.

13: If we applied their method directly, 

14: we would have to solve an exponentially sized system of abstract semantic equations, 

15: resulting in memory exhaustion.

16: Instead, we keep the system implicit and discover strategy improvements

17: using SAT modulo real linear arithmetic (SMT).

18: For evaluating strategies we use linear programming.

19: Our algorithm has low polynomial space complexity 

20: and performs for contrived examples in the worst case exponentially many strategy improvement steps; 

21: this is unsurprising,  since we show that the associated abstract reachability problem is $\Pi^p_2$-complete.

22: \end{abstract}

23: