Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF
Alessandro Cimatti Alberto Griggio Ahmed Irfan Marco Roveri Roberto Sebastiani
cs.LO





























fmpage[1]
#1
























































  








 

















CEGAR VMT  





Fondazione Bruno Kessler, Italy,

@fbk.eu,

University of Trento, Italy,

@unitn.it






















Invariant Checking of NRA Transition Systems

via Incremental Reduction to LRA with EUFThis work was performed as part of the H2020-FETOPEN-2016-2017-CSA project SC^2 (712689).







    Alessandro Cimatti1
Alberto Griggio1 Ahmed Irfan1,2 
 Marco Roveri1 Roberto Sebastiani2
    
===========================================================================================================================================================================================================






Model checking invariant properties of designs, represented as
transition systems, with non-linear real arithmetic (NRA), is an
important though very hard problem. On the one hand NRA is a
hard-to-solve theory; on the other hand most of the powerful model
checking techniques lack support for NRA. In this paper, we present a

counterexample-guided abstraction refinement (CEGAR)
approach that 

leverages linearization techniques from differential calculus to
enable the use of mature and efficient model checking algorithms 
for
transition systems on linear real arithmetic (LRA) with uninterpreted functions (EUF).

The results of an empirical evaluation  confirm the validity and potential of this approach.






§ INTRODUCTION



Invariant checking for infinite-state transition systems is a
fundamental research area. Based on the recent improvements of SMT
technologies, effective approaches have been developed for the case of
transition systems with dynamics over Linear Real
Arithmetic <cit.>.

However, many real-world industrial designs (e.g.  aerospace,
automotive) require modeling as transition systems over non-linear
arithmetic (NRA).

Although both problems are undecidable, proving properties of the NRA
transition systems turns out to be much harder than the linear case,
and has in fact received much less attention.

Approaches based on BMC and k-induction <cit.> are possible, so that
non-linearity is handled at the SMT-level, by means of an SMT(NRA)
solver (e.g. Z3 <cit.>, nlSAT <cit.>,
Yices <cit.>, SMT-RAT <cit.>).




Their power is however limited. Consider the following simple
transition system: initially, x ≥ 2 ∧ y ≥ 2 ∧ z =
x*y; the transition relation is defined by x'= x + 1 ∧ y' = y +
1 ∧ z' = x'*y'.  The property “it is always the case that
  z ≥ x + y” is not k-inductive, not even for a very large
value of k. Thus, the typical proving techniques that are based
on k-induction using an SMT(NRA) solver will not be able to prove it.

In principle, it is also possible to lift other approaches
(e.g. interpolation, IC3 <cit.>) to handle
non-linearities at the level of the solver. However, this requires the
SMT(NRA) solver to carry out interpolation or quantifier elimination,
and to proceed incrementally. These extra functions are usually not
available, or they have a very high computational cost.

In this paper, we propose a completely different approach to tackle
invariant checking for NRA transition systems. Basically, we work with
an abstract version of the transition system, expressed over LRA with
EUF, for which we have effective verification tools <cit.>.

In the abstract space, nonlinear multiplication is modeled as an
uninterpreted function. When spurious counter-examples are found, the
abstraction is tightened by the incremental introduction of linear
constraints, including tangent planes resulting from differential
calculus, and monotonicity constraints.

We implemented the approach on top of the model
checker <cit.>, leveraging the IC3 engine with Implicit Abstraction <cit.> for invariant
checking of transition systems over LRA with EUF.

We compared it, on a wide set of benchmarks, against multiple
approaches working at NRA level, including BMC and k-induction using
SMT(NRA), the recent interpolation-based engine <cit.>, and
the static abstraction approach proposed in <cit.>. The
results demonstrate substantial superiority of our approach, that is
able to solve the highest number of benchmarks.

The effectiveness of our approach is possibly explained with the
following insights. On the one hand, in contrast to LRA, NRA is a
hard-to-solve theory: in practice, most available complete solvers rely on CAD
techniques <cit.>, which require double exponential
time in worst case. Thus, we try to avoid NRA reasoning, trading it
for LRA and EUF reasoning.

On the other hand, proving properties of practical NRA transition
systems may not require the full power of non-linear solving. In fact,
some systems are “mostly-linear” (i.e.  non-linear constraints are
associated to a very small part of the system), an example being the Transport Class Model (TCM) for aircraft simulation from the Simulink model library <cit.>.

Furthermore, even NRA transition systems with significant non-linear
dynamics may admit a piecewise-linear invariant of the transition
system that is strong enough to prove the property.







Structure. In Sec. <ref> we discuss the
related work, and in Sec. <ref> introduce some
background.  In Sec. <ref> we discuss the approach in
the setting of SMT(NRA). In Sec. <ref> we present the
verification algorithm for NRA transition systems. In
Sec. <ref> we describe the results of the experimental
evaluation.  In Sec. <ref> we conclude and outline the
directions for future research.



§ RELATED WORK



There are not many tools that deal with NRA transition systems.

The most relevant is the recently proposed
 <cit.>, that uses an
interpolation-based <cit.> approach to
prove invariants. In addition to NRA, it also supports trascendental
functions and some form of differential equations.  is
built on an SMT solver based on numeric techniques (interval
arithmetic), and is able to provide results that are accurate up to
the specified precision. In fact, in addition to “safe” and
“unsafe” answers, may return “maybe unsafe” when it
finds an envelope of given precision that may (but is not guaranteed
to) contain a counterexample.

Another relevant tool is  <cit.>, a bounded
model checker implemented on top of the  <cit.> SMT
solver, that adopts numerical techniques similar to
. has an expressiveness similar to , but
being a bounded model checker it is unable to prove properties.

The work in <cit.> follows a reduction-based approach to
check invariants of transition systems. It over-approximates the
non-linear terms with a coarse abstraction, encoding into some weak
properties of multiplication like identity and sign.

Another reduction-based approach is presented
in <cit.> in the context of program
analysis. The idea is to find a (tighter) convex
approximation of polynomials in form of polyhedra, thus obtaining a
conservative linear transition system.


The key differences of our approach with respect
to <cit.> are that we iteratively
refine the abstraction, and we adopt a reduction to .

Furthermore, to the best of our knowledge, there is no available
implementation of the approach <cit.> in a
program analysis tool – it has been only shown to work on SMT
problems.

The idea of approximating a univariate function (in particular the
natural logarithm ln) with tangent lines is used
in <cit.>. Here we abstract a bivariate function
(multiplication), and use tangent planes for the refinement. We
also exploit other properties (e.g. monotonicity) to derive additional axioms.

The idea of using tangent planes (spaces) has been explored
in <cit.>, limited to the case of SMT
solving. Another key differences is that the tangent planes area used
to under-approximate predicates, while we use them to refine the
over-approximation of the multiplication function.






































§ BACKGROUND





  §.§.§ Properties of the Multiplication Function.












Geometrically, the surface generated by the multiplication function 
f(x,y)  x * y is shown in Fig. <ref> and <ref>.

This kind of surface is known in geometry as hyperbolic paraboloid.
A hyperbolic paraboloid is a doubly-ruled surface, i.e. for every
point on the surface, there are two distinct lines projected from the
surface such that they pass through the point. In case of the
multiplication surface, the projected lines basically lie on the
surface.



  
Tangent Plane.
The tangent plane to a surface at a point of interest (a,b) is a
plane that “just touches” the surface at the point. The tangent
planes can be used to linearly approximate the surface at the point of
interest. An important property of the tangent plane to a hyperbolic
paraboliod is that the two projected lines from the surface are also
in the tangent plane, and they define how the plane cuts the surface
(see
Fig. <ref> and <ref>).
The tangent plane x,ya,b to the multiplication function
f(x,y) at point (a,b) is calculated as follows:


    x,ya,b f(a,b)     +  f(x,y)x_|_(a,b)*(x - a) +  f(x,y)y_|_(a,b)*(y - b)

where f(x,y)x_|_(a,b) and f(x,y)y_|_(a,b) are the first-order partial
derivatives of f(x,y) w.r.t. x and y respectively, evaluated at (a,b).

x,ya,b simplifies to:

    x,ya,b b*x + a*y - a*b













  §.§.§ Logic and Satisfiability.


We assume the standard first-order quantifier-free logical setting and
standard notions of theory, model, satisfiability, and logical consequence. 

If φ is a formula, 
we denote with φ the set of its variables,
and with φ the set of its atoms.
We write φ(X) to denote that φ⊆ X.

If x and y are two variables, we denote with φxy 
the formula obtained by replacing all the occurrences of x in φ with y. 
We extend this notation to ordered sequences of variables in the natural way.

If μ is a model and x is a variable, we write μ[x] to denote the value of x in μ, 
and we extend this notation to terms in the usual way.

If X is a set of variables, 
we denote with X' the set obtained by replacing 
each element x ∈ X with x', 
and with Xi the set obtained by replacing x with xi.

If Γ is a set of formulas, 
we write ⋀Γ to denote the formula obtained by taking the conjunction of all its elements.

If ⋀Γ is unsatisfiable (modulo some theory T), 
an unsatisfiable core is a set C ⊆Γ such that ⋀ C is still unsatisfiable.



  §.§.§ Symbolic Transition Systems.



A symbolic transition system X, I, T 
is a tuple where X is a finite set of (state) variables,
I(X) is a formula denoting the initial states of the system,
and T(X,X') is a formula expressing its transition relation.
A state s_i of  is an assignment to the variables X.
A path (execution trace) π = s_0,s_1,s_2,…,s_k-1 of length k 
(possibly infinite)
for  is a sequence of states 
such that s_0  I and 
s_i s_i+1XX' T for all 0 ≤ i < k-2.
We call an unrolling of  of length k the formula 
IXX0⋀_i=0^k-1TXXiX'Xi+1.

Let P(X) be a formula whose assignments represent a property (good
states) over the state variables X. 
The invariant verification problem,
denoted with S P, is the problem of checking if for all the
finite paths
s_0,s_1,…,s_k of , for all i, 0≤ i≤ k,
s_i P.
Its dual formulation in terms of reachability of P is the
problem of finding a path s_0,s_1,…,s_k of  such that
s_k P. P represents the “good” states, while
P represents the “bad” states.




















































§ SOLVING SMT() VIA SMT()







  §.§.§ Top-level Algorithm.


The main idea of this paper is that of solving an SMT formula
containing non-linear polynomial constraints (i.e., expressed in the
theory) by overapproximating it with a formula over the combined
theory of linear arithmetic and uninterpreted functions ().

Our main SMT solving procedure follows a classic abstraction refinement loop,
in which at each iteration the current overapproximation of the input SMT formula
is refined by adding new constraints that rule out one (or possibly more) spurious solutions,
until one of the following occurs:
(i) the SMT formula becomes unsatisfiable in the theory; or
(ii) the model for the current overapproximation can be lifted to an model for the original SMT formula; or
(iii) the resource budget (e.g. time, memory, number of iterations) is exhausted.

The pseudocode for the top-level algorithm is shown in Fig. <ref>.
We provide more details about its main components in the rest of this section.

pseudocodecounter

 








  §.§.§ Initial Abstraction.



The function takes as input an SMT() formula φ
and returns an overapproximation φ of it in the theory.

First, each multiplication expression x * y
between two variables
[To simplify the presentation, we assume (here and in the rest of the paper)
that all multiplications in φ
are either between two variables or between one constant and one variable.
]

occurring in φ is replaced by x,y,
where  is a binary uninterpreted function returning a real.
We remark that this happens only for non-linear multiplications:
expressions like c * x or x * c in which c is a constant are not rewritten.

Then, some simple axioms about multiplication are added to φ
via static learning. For each x,y∈φ, we add the following axioms:

    Commutativity:    x,y = y,x
    Sign:    x,y = -x,-y∧x,y = --x,y 
       x,y = -x,-y
    Zero:     ((x = 0  y = 0) ↔x,y=0)  
        (((x > 0 ∧ y > 0) ∨ (x < 0 ∧ y < 0)) →x,y > 0)  
        (((x < 0 ∧ y > 0) ∨ (x < 0 ∧ y > 0)) →x,y < 0)





  §.§.§ Abstraction Refinement.



If the SMT check on the abstraction returns false
(line <ref> of Fig. <ref>),
we can conclude that the input formula is unsatisfiable. In this case,
Γ contains all the lemmas (discussed later in this section)
that were added in the earlier refinements (line <ref> of
Fig. <ref>).

Otherwise, we have to check whether the model μ
found for φ is also a model for the original
formula φ.

Let Fmuls be the set of all x,y terms occurring in φ.
In its simplest version,
the function checks whether, for all x,y in Fmuls,
μ[x,y] = μ[x] * μ[y].
If this is the case, then μ is also a model for the original formula,
and returns true.
(We present more sophisticated versions of below.)

Otherwise,
let CFmuls be the set of all x,y terms whose value in μ
is different from μ[x] * μ[y].
The function generates a set of axioms Γ' such that

there exists at least one element x,y of CFmuls
such that
the formula
φ⋀Γ' has no model μ'
that agrees with μ on the values of x,y and x,y
(i.e. such that
μ'[x,y] = μ[x,y],
μ'[x] = μ[x] and
μ'[y] = μ[y]).
Intuitively, the axioms Γ' block the bad model values for x,y,
making the abstraction more precise by restricting the set of spurious solutions.

In our current implementation, two kinds of lemmas are generated during refinement:
tangent lemmas and monotonicity lemmas.



  
Tangent Lemmas.
We use the model values μ[x,y], μ[x] and
μ[y] and (<ref>) to generate tangent
plane lemmas for x,y:


    a,y = a * y     x,b = b * x   
       (((x > a ∧ y < b) ∨ (x < a ∧ y > b)) →x,y <  x,ya,b)    
    
       (((x <  a ∧ y < b) ∨ (x >  a ∧ y >  b)) →x,y >  x,ya,b)


where we can choose a and b as:


    a μ[x]  and  b μ[y] 
       a 1/μ[x,y] and  b μ[y] 
       a μ[x]  and  b 1/μ[x,y].

Basically the equalities in the tangent lemma are providing
multiplication lines that enforce the correct value of x,y when
x=a or y=b. Moreover, the inequalities of the tangent lemma are
providing bounds for x,y when x and y are not on the
multiplication lines.



  
Monotonicity Lemmas.
Let x,y and w,z be two terms in φ, such that
μ[x]≤μ[w],
μ[y]≤μ[z], and
μ[x,y] > μ[w,z].
Then, we add the monotonicity lemma

    (abs(x) ≤ abs(w) ∧ abs(y) ≤ abs(z)) → abs(x,y) ≤ abs(w,z),

where abs(t) stands for (t < 0, -t, t).






  §.§.§ Finding Models.





It is easy to see that our algorithm

 is expected to perform much better
for unsatisfiable instances than for satisfiable ones.
The algorithm can return true (meaning that the formula is satisfiable)
only if the solver “guesses” a model
that is consistent with all the nonlinear multiplications.
In an infinite and dense domain like the reals,
the chances that this will happen are close to zero in general.

Moreover, our approach is inherently limited,
because it can only find models over the rationals.
If the input formula is satisfiable,
but all its models contain some irrational values,
then our algorithm will always abort
(or never terminate, if there is no resource budget set).
In practice, it is very likely that the same will happen
even for formulas admitting a rational solution.

One possibility for addressing this limitation would be to couple our procedure
with a complete solver for , to be used for detecting satisfiable cases,
in order to implement a more effective version of .
One such possibility is shown in Fig. <ref>,
where we extract the truth assignment ψ induced by
the model μ on the atoms of φ:

    ψ⋀_[a_i∈φ s.t. μa_i]a_i  ∧ ⋀_[a_i∈φ s.t. μa_i]a_i,

We concretize it by replacing each x,y in ψ with x*y,
and invoke
the complete theory solver on the resulting conjunction of -literals
ψ,
to check whether it contains at least one solution.

Although in general the problem is expected to be simpler than the
original input formula because the Boolean structure of
φ is disregarded, invoking a complete theory solver at each loop
iteration of could be very expensive.  Moreover,
this would still require a complete theory solver, which might not
always be available.








As an alternative, we propose the procedure
outlined in Fig. <ref>,
where we extract the truth assignment ψ induced by
the model μ on the atoms of φ,
and we conjoin to it the multiplication lines:

    ψ^*
        =    ψ ∧⋀_x,y∈ Fmuls (
      [ ( x = μ[x] x,y = μ[x] * y ); ( y = μ[y] x,y = μ[y] * x ) ] ),

Fmuls being the usual set of all x,y terms occurring in φ.

The main idea is to build an LRA+EUF underapproximation ψ^* of the
NRA formula ψ of Fig. <ref>, in which all
multiplications are forced to be linear. 








Compared to the previous solution, this has the advantage of
requiring a complete SMT(LRA+EUF) solver rather than a (much more expensive)
complete solver.
  Moreover, given the simplicity of
the Boolean structure of the underapproximated formula, the check
should in general be very cheap. 
The drawback is that this is
(clearly) still an incomplete procedure.  However, in our experiments
(for which we refer to Sec. <ref>) we have found it to be
surprisingly effective for many problems.




































Unlike with the basic implementation of



which considers
  only one single candidate
  model at a time, the implementations in
  Fig.<ref> and
  Fig. <ref> consider an
  infinite amount of them, drastically increasing the chances of
  finding a model.



  
Correctness and progress.
  We notice that the procedure in Fig. <ref> is
  correct. In fact, it returns false only if φ is
  NRA-unsatisfiable because by construction φ is  an
  over-approximation of φ, and all axioms in Γ
  are valid in any theory interpreting x,y as x * y.

  Also, it returns true only if  is NRA-satisfiable:




  * if 
  is based only on evaluation,
  
  
  then by construction
  μ is an LRA+EUF-model for
  φ s.t. each x,y equals x*y in μ,
  so that μ is also a model for φ;


  * if  is as in Fig. <ref>,
then μ is an NRA-model of a conjunction of literals ψ which
tautologically entails , so that μ is a model for ;


  * if  is as in Fig. <ref>,
then μ is an LRA+EUF-model of a conjunction of literals
ψ^* which
tautologically entails  and it is s.t. each x,y
equals x*y in μ, so that μ is a also model for .
  

We also notice that the progress of the procedure in
Fig. <ref> is guaranteed by the refinement step,
which rules out significant parts of the search space at every loop by
means of the added lemmas.









  §.§.§ Important Heuristics for Refinement.



The description of provided above leaves some flexibility
in deciding what axioms to add (and how many of them) at each iteration.
It is possible to conceive strategies with an increasing degree of eagerness,
from very lazy (e.g. adding only a single axiom per iteration)
to more aggressive ones.
In our current implementation, we eagerly add all the axioms (<ref>)–(<ref>)
that are violated by the current abstract solution μ,
leaving the investigation of alternative strategies as future work.

However, we found the following two strategies to be crucial for performance.



  
Tangent lemma frontiers.

The tangent lemmas of (<ref>) for a given point (a, b)
are based on the fact that the multiplication function x*y is a hyperbolic paraboloid surface,
and a tangent plane to such surface cuts the
surface into four regions such that in two of the regions the tangent plane
is above the surface, whereas in the other two regions the tangent
plane is below the surface (see Fig. <ref>).

Each instantiation of (<ref>) for a given point, therefore,
can only provide either a lower or an upper bound for a given region.
In some cases, this might lead to an infinite refinement loop
in which at each iteration the “wrong” bound is refined.

In order to address the problem, we use the following strategy.

For each x,y in the input formula, we maintain a frontier l_x, u_x, l_y, u_y
with the invariant that whenever x is in the interval [l_x, u_x]
or y is in the interval [l_y, u_y],
then x,y has both an upper and a lower bound.

Initially, the frontiers are set to 0,0,0,0.
Whenever a lemma (<ref>) for x,y is instantiated on a point (a, b),
we generate further instantiations of (<ref>) and update the frontier as follows:


  case a < l_x and b < l_y: instantiate (<ref>)
  on (a, u_y) and on (u_x, b), and set the frontier to a, u_x, b, u_y;

  case a < l_x and b > u_y: instantiate (<ref>)
  on (a, l_y) and on (u_x, b), and set the frontier to a, u_x, l_y, b;

  case a > u_x and b > u_y: instantiate (<ref>)
  on (a, l_y) and on (l_x, b), and set the frontier to l_x, a, l_y, b;

  case a > u_x and b < l_y: instantiate (<ref>)
  on (a, u_y) and on (l_x, b), and set the frontier to l_x, a, b, u_y.


Fig. <ref> shows a graphical illustration of the strategy.





  
Tangent lemma rounding.

The instantiation of a tangent lemma at the point (a, b)
has the side-effect of adding the rational constants a, b and a*b
to the formula that is solved by the solver.
If such values have large numerators and/or denominators,
they might be a source of a significant slow-down for the solver
(which works on exact, arbitrary-precision rational arithmetic).

We address this issue by observing that,
in order to block a bad model μ such that
μ[x,y] ≠μ[x] * μ[y],
it is sufficient to add one of the two equalities of (<ref>);
therefore, instead of instantiating a tangent lemma at (a, b),
we can instantiate it at either (a+δ, b) or at (a, b+δ),
for any value of δ.

In practice, if a (resp. b) is a rational constant with a very large numerator or denominator,
instead of instantiating a tangent lemma at (a, b),
we instantiate two tangent lemmas at (⌊ a ⌋, b) and (⌈ a ⌉, b).



§ FROM SATISFIABILITY TO VERIFICATION







We now move from satisfiability checking to verification.



  §.§.§ Overview.


In principle, the solver described in the previous section could be integrated
as a “black box” in any off-the-shelf SMT-based verification algorithm,
such as BMC, k-induction, or one of the many extensions of IC3 to the SMT case (e.g. <cit.>).

In practice, however, such black-box integration would hardly be effective,
especially in the case of state-of-the-art algorithms like IC3.
IC3 requires a very incremental interaction with the underlying SMT engine,
which is asked to solve a large number of relatively-cheap queries.
The procedure of Sec. <ref>, however, can be very expensive, especially for satisfiable queries,
which are very common in an IC3-like algorithm.
[In fact, as already discussed in Sec. <ref>,
the procedure is biased towards unsatisfiable instances,
and might easily diverge on satisfiable ones.]
Moreover, some of the IC3 extensions mentioned above require the ability
of performing (approximated) quantifier eliminations,
a functionality not provided by the algorithm of Fig. <ref>.

We propose therefore a white-box integration,
in which we lift the abstraction refinement approach of
Sec. <ref> at the transition system level.
We generate an abstract version of the input transition system,
which is then checked with the IC3-based procedure of <cit.>.
In case a counterexample is produced,
we use the algorithm of Fig. <ref>
to check whether it is spurious.
If so, the axioms generated by are then used to refine the abstraction of the transition system.
The pseudo-code of this algorithm is reported in Fig. <ref>.
Similarly to the satisfiability checking case, the  function
replaces every non-linear multiplication x*y in the input transition system and property with a x,y term,
and adds some simple axioms about the behaviour of multiplication
 to the initial-state and transition-relation formulas of the transition system (see Sec. <ref>).
In the rest of this section,
we describe the abstraction refinement algorithm in more detail.






  §.§.§ Counterexample Checking and Refinement.




When returns a counterexample trace π
for the abstract system ,
we use to check for its spuriousness.
The function builds a formula ψ to feed to ,
whose unsatisfiability implies that π is spurious.
The formula ψ is built by unrolling the transition relation of ,
and optionally adding constraints that restrict the allowed transitions
to be compatible with the states in π.
Various heuristics are possible, trading generality for complexity:
ψ could be fully constrained by the states in π (thus checking only one abstract counterexample path per iteration);
it could be only partially constrained
(e.g. by considering only the Boolean variables and/or the state variables occurring only in linear constraints);
or it could be left unconstrained,
considering only the length of the abstract counterexample.

In our current implementation (see Sec. <ref>),
we use the last option,
i.e. we only consider the length of π
to build a BMC formula that checks for any counterexample of the given length,
leaving the investigation of alternative strategies to future work.

If returns true, the property is violated.
In this case, we can use the model found by to build a counterexample trace for the input system and property.

If returns false,
we use the axioms Γ produced during search to refine the transition system ,
using the procedure shown in Fig. <ref>.

Essentially, translates back the axioms from their unrolled version (i.e. on variables X0, X1, …) to their “single step” version
(on variables X and X'), adding each of them
either to the initial-states formula or to the transition relation formula.
In case an axiom γ spans more than a single transition step (lines <ref>–<ref>
of Fig. <ref>),
we arbitrarily choose to map the variables with the lowest index as current state variables X, and all the others as next-state variables X'.
Notice that this might cause some refinement failure, as discussed in the next paragraph.




  
Reducing the number of axioms to add.

In general, not all the axioms generated during a call to are needed to successfully block a counterexample,
especially if eager strategies like those described in Sec. <ref> are used.
In the long run, having a large number of redundant axioms can be quite harmful for performance.
In order to mitigate this problem,
we apply a filtering strategy (based on unsatisfiable cores)
to the set of axioms, before adding them to the transition system.
Instead of adding Γ_I and Γ_T directly to ,
we invoke the function shown in Fig. <ref>.

Note that due to the flattening of multi-step axioms described above
(lines <ref>–<ref>
of Fig. <ref>), the refinement might fail.

In this case, our current implementation simply aborts the execution.
[We remark however that so far we have never observed this behaviour during our experiments.]





§ EXPERIMENTAL ANALYSIS







  §.§.§ Implementation and comparisons.

We have implemented a prototype of the procedure 
using
the engine of  <cit.> for .
The code is written in Python, 
using the library <cit.>.

Our implementation, benchmarks, and experimental data are available at
<https://es-static.fbk.eu/people/griggio/papers/tacas17-ic3-nra.tar.gz>.

We have used the following tools for our evaluation.








:
we apply the upfront abstraction of to proposed in <cit.>,
running the engine of on the resulting transition system.












-{, } and  -{, }:
we have implemented the  <cit.> and 
 <cit.> algorithms in Python (using ),
using either () or () as back-end SMT solver.








and :
we have used the latest version of the solver <cit.>,
which combines an SMT solver integrating CDCL and interval constraint propagation techniques
with an interpolation-based abstaction/refinement algorithm for verification.
supports both transition systems and software programs encoded as
control flow graphs.








Similarly to ,
may return a “maybe unsafe” answer and provide a
candidate solution identifying the upper and lower bounds on the
variables. 


In the experiments,
is the configuration suggested by the authors
[
0.8
0.8
0.8]
and is the same except that the minimum splitting width ()
parameter is set to 10^-9. 
We have used a smaller value for the  to get more precise answers, 
i.e. “safe” or “unsafe”, as suggested in the user manual.




  §.§.§ Benchmarks.

We have collected a total of 114 benchmarks from various sources.










Handcrafted. 
This set contains 14 hand-written instances, 13 safe and 1 unsafe.








HyComp.
The second set contains 7 benchmarks (3 safe, 4 unsafe)
which are taken
from <cit.> and converted to transition
systems using  <cit.>.




HYST.
This is the biggest set, consisting of 65 benchmarks.
These are generated from the Hybrid examples that come with the
 <cit.> distribution, by approximating the continuous
time by sampling at a fixed time interval. This process is done
automatically using an extended version of . Since the generated
benchmarks are approximations, we do not know their safety status. The
benchmarks contain mostly non-linear behaviour.





iSAT3 and iSAT3-CFG.
The 11 benchmarks in this set (7 safe, 4 unsafe)
are taken from <cit.> and the examples available online. 




nuXmv.
In this set, we have 2 safe benchmarks which we collected from the
nuXmv users' mailing list. 
These benchmarks have complex boolean structure.

SAS13.
These 13 benchmarks are generated from the C programs used in <cit.>, 
but interpreted over NRA instead of the theory of IEEE floating-point numbers. 
This makes some of the instances unsafe.











TCM.
We have generated 2 safe benchmarks from the Simulink models (taken
from the case study <cit.>) by first generating the
C code using the Embedded
Coder[<https://www.mathworks.com/products/embedded-coder/>]
and then encoding the program into a symbolic transition system.




  §.§.§ Results.
 
















We ran our experiments on a cluster of machines with 2.67GHz Xeon
X5650 CPUs and 96GB of RAM, running Scientific Linux 6.7. We used 6GB
memory limit and 3600 seconds CPU timeout.

The results are summarized in Tables <ref> and <ref> 
and in Fig. <ref>. 
The plots show 


the time to solve an
instance on the x-axis and the total number of solved
instances on the y-axis. 

Table <ref> reports a summary of the solved instances by family,
whereas




Table <ref> shows
a comparitive analysis by reporting for each tool the number of uniquely solved instances and the difference of solved instances w.r.t
.




We can make the
following observations from the experimental results:


  * is the best performer overall,
  and it significantly outperforms all the other approaches on safe instances (where it can solve 9 problems that are out of reach for all the other tools).
Interestingly, despite its simplicity, 
our model finding approach (as outlined in sec:cegar-nra-smt)
is surprisingly effective, allowing to find 15 counterexample traces.













  * The simple abstraction proposed in <cit.> is quite effective for many families,
allowing to verify more properties than the approaches based on K-induction with an solver.
However, results in a clear and very significant improvement, 
solving more than twice as many instances than (and losing only 1).






  * None of the other tools (with the exception of ) 
  is able to solve any safe benchmark in the HyComp and nuXmv families.
  These benchmarks have a non-trivial Boolean structure and a significant linear component. 
  Both and are able to fully exploit the effectiveness of the underlying engine of ,
  outperforming the competitors.
  
  However, is very competitive also on the HYST family, 
  whose instances are mostly non-linear and have very little Boolean structure. 






  * Increasing the default precision of significantly reduces the number of “maybe unsafe” answers,
but it doesn't seem to help in solving more benchmarks.
In fact, we remark that even with the increased precision classifies 2 safe instances as “maybe unsafe” (whereas in the default configuration, 6 safe instances are classified as “maybe unsafe”).

























§ CONCLUSIONS AND FUTURE WORK



We presented a novel abstraction-refinement approach to the
verification of transition systems with nonlinear dynamics expressed
in the NRA theory. We abstract non-linear multiplication as an
uninterpreted function, leveraging efficient invariant checkers for
transition systems over LRA and EUF to solve the problem in the
abstract space. In case of spurious counterexample, the abstraction of
multiplication is incrementally refined by introducing suitable
axioms, based on the idea of tangent planes.

An extensive experimental evaluation demonstrates that the proposed
approach is significantly more effective than approaches directly
based on SMT(NRA) solving.




This work opens up several important directions.

First, we are going to improve the implementation, by integrating all
the steps within the  <cit.> model checker, and to perform
a thorough analysis of the various heuristic choices.

Second, we will investigate the potential of the approach for
SMT, both for other theories (e.g. NIA) and for extended functionalities
(e.g. interpolation).

We will also extend the scope of the approach to deal with
transcendental functions, look-up tables, and partially axiomatized
functions (e.g. gain functions known to be monotonic and of restricted
co-domain).



Finally, we are going to investigate the generalization of the
approach from transition systems to continuous-time hybrid systems
with nonlinear characteristic functions.



  
Acknowledgement.
We greatly thank the team for providing the latest
executable and iSAT3-CFG benchmarks. We also thank James
Davenport for the fruitful discussions on CAD techniques
and finding solutions in NRA.





plain














