# Linear Overapproximaion of Nonlinear Transactions

# Problem statement
We show to utilize SMT solvers for automatically extracting overapproximations of loop free code transactions.

# Setting
We assume that C is a loop-free code block over variables *v1, v2, vk.* *E(v1, v2, ..., vk, v'1, v'2, ..., v'k)* is a (nonlinear) formula over intergers which describes the effect of C. *A(v1, v2, ..., vk, v'1, v'2, ..., v'k)* is a numerical abstract domain over the 2k variables (e.g., octagon or Polyhedra).

# A Naive Algorithm

Below we describe a naive algorithm for generating an over-approximation of code using SMT solvers. We assume that the abstract domain supports three operations:
1. An operation beta for computing the most precise overapproximation of a signleton state.
2. An operation join for joining two astract values.
3. An operation toformula which converts an abstract value into a formula over integers.

The SMT solvers returs pairs <s, s'> that is a model of the transition formula and is not covered by the current approximation.
This algorithm is naive since the number of iterations may be high. Widening can be applied but this may entail loss of precision. Another possibility is use disjunctions by statically analyzing paths in the DAG of the code block.

 res = *bottom* // Start with the bottom of the domain
 while there exists s, s' such that <s, s'> |= 
                                    E(v1, .., vk, v;1, .., v'k) /\ ! toformula(res)
    res := res join beta(s, s')

## notes (by alex)

- The abstract states here are two-state formulas (called summaries by some) -- we require at least a relational domain to state anything reasonable, most probably (which octagons and polyhedra are).
- Much will depend on the widening. Are quantifier elimnation (or interpolation) techniques a natural tool to use here?
- In principle, we don't always need a full overapproximation of the transition formula. E.g. <s,s'> |= E, but s is unreachable at E's starting location, or s' never leads to an error.