=Paper=
{{Paper
|id=Vol-259/paper-15
|storemode=property
|title=A Sequent Calculus for Integer Arithmetic with Counterexample Generation
|pdfUrl=https://ceur-ws.org/Vol-259/paper15.pdf
|volume=Vol-259
|dblpUrl=https://dblp.org/rec/conf/cade/Rummer07
}}
==A Sequent Calculus for Integer Arithmetic with Counterexample Generation==
<pdf width="1500px">https://ceur-ws.org/Vol-259/paper15.pdf</pdf>
<pre>
A Sequent Calculus for Integer Arithmetic with
        Counterexample Generation

                                      Philipp Rümmer
                     Department of Computer Science and Engineering,
             Chalmers University of Technology and Göteborg University, Sweden
                                    philipp@chalmers.se



     Abstract. We introduce a calculus for handling integer arithmetic in first-order logic.
     The method is tailored to Java program verification and meant to be used both as a sup-
     porting procedure and simplifier during interactive verification and as an automated tool
     for discharging (ground) proof obligations. There are four main components: a complete
     procedure for linear equations, a complete procedure for linear inequalities, an incom-
     plete procedure for nonlinear (polynomial) equations, and an incomplete procedure for
     nonlinear inequalities. The calculus is complete for the generation of counterexamples
     for invalid ground formula in integer arithmetic. All parts described here have been
     implemented as part of the KeY verification system.



1   Introduction
We introduce a Gentzen-style sequent calculus for integer arithmetic that is
tailored to integrated automated and interactive Java software verification. The
calculus was developed for dynamic logic for the Java language [1, Chapter 3] (a
classical first-order logic) and integrates well-known as well as new algorithms,
with the goal to meet the following features:
– Simplification of arithmetic expressions or formulas with the goal to keep
  everything small and readable. A calculus for this purpose should always
  terminate and should not cause proof splitting; completeness is a secondary.
– Transparency and the ability to create human-readable proofs and sequences
  of simplification steps, otherwise it is difficult for a user to resume interac-
  tive proving after a number of automated proof steps. The fastest way to
  understand a proof goal is often to look at the history that led to the goal.
– Handling of nonlinear arithmetic guided by the user, which is necessary for
  programs that happen to contain multiplication or division operations. The
  cost of interactive software verification should be justified by the ability to
  also handle more complex programs than automatic tools.
– Generation of counterexamples for invalid formulas, which is useful during
  specification and when proving with induction and invariants.
– Handling of the actual modular Java integers, which in our system is modelled
  by a mapping to the mathematical integers [1, Chapter 12]. Reasoning in
  this setting requires good support for simplifying expressions, for instance by
180     Philipp Rümmer


  (implicitly) proving the absence of overflows. The methods that we developed
  to this end are beyond the scope of the paper, but are based on the presented
  calculus.
– Most importantly: it should be easy to use!
    Only some of these points can be solved using external procedures and the-
orem provers (which are, nevertheless, extremely useful for dealing with simpler
proof obligations). As a complementary approach, we have developed a novel cal-
culus for integer arithmetic that is directly implemented in our theorem prover
KeY [1] in form of derived (i.e., verified) proof rules. The rules are deliberately
kept as elementary as possible and are here presented in sequent calculus nota-
tion. The calculus is driven by a proof strategy that controls the rule application
and realises the following components: (i) a simplification procedure that works
on single terms and formulas and is responsible for normalisation of polynomi-
als (Sect. 2), (ii) a complete procedure for systems of linear equations, based
on Gaussian elimination and the Euclidian algorithm (Sect. 3), (iii) a complete
procedure for systems of linear inequalities, based on Fourier-Motzkin variable
elimination (Sect. 4), (iv) an incomplete procedure for nonlinear (polynomial)
equations, based on Gröbner bases (Sect. 5), (v) an incomplete procedure for
nonlinear inequalities using cross-multiplication of inequalities and systematic
case analysis (Sect. 6).
    The development of the method was mostly an engineering process with the
goal of handling cases that practically occur in Java program verification. It was
successful in the sense that many proofs that before only were possible with the
help of external provers can now be handled by KeY alone (e.g., the case study
[2]), and that many proofs that before were impossible have become feasible.
    We do not consider quantifiers or uninterpreted functions in this paper. The
calculus is proof confluent (cf. [3]) and can basically be used in two different
modes: (i) for simplification, which disables the handling of nonlinear inequal-
ities, prevents case splits and guarantees termination (Procedure 4 in Sect. 5),
and (ii) for proving and countermodel construction, which enables all parts (Pro-
cedure 5 in Sect. 6).

Introductory example. We start with an example and show how the following
statement can be proven within our calculus (in the “full” mode):1
             .
   11a + 7b = 1 ⊢ h b=a*c-1; if (c>=a) a=a/b; i true                  (1)
In Java dynamic logic, this sequent expresses that the program in angle brack-
ets terminates normally, i.e., in particular does not raise exceptions, given the
                     .
assumption 11a + 7b = 1. A proof is conducted by rewriting the program follow-
ing the symbolic execution paradigm [4], whereby the calculus presented in this
1
    On an Intel Pentium M processor with 1.6 GHz, the KeY implementation of the procedure needs
    about 460 inference steps and 2 seconds to find this proof.
              A Sequent Calculus for Integer Arithmetic with Counterexample Generation         181


                                    .                  .         .      .            .
                                5c ≥ −7e − 8, e ≤ −1, c ≤ −1, c ≥ 7e + 2, 7ce = −2c + 1 ⊢    (13)
                                  .                      .         .      .            .
                              ce ≥ −c − e − 1, e ≤ −1, c ≤ −1, c ≥ 7e + 2, 7ce = −2c + 1 ⊢   (12)
                                              .          .         .          .
                                            e ≤ −1, c ≤ −1, c ≥ 7e + 2, 7ce = −2c + 1 ⊢      (11)
                                                     .       .              .
                    ···                           c ≤ −1, c ≥ 7e + 2, 7ce = −2c + 1 ⊢        (10)
                                                .              .
                                    . . . , c ≥ 7e + 2, 7ce = −2c + 1 ⊢                      (9)
                        .                 .                .                       .
                     a = 7e + 2, b = −11e − 3, c ≥ 7e + 2 ⊢ 7ce + 2c − 1 6= 0                (8)
              .             .                      .
   ···     a = 7e + 2, b = −11e − 3, c ≥ 7e + 2 ⊢ {b := 7ce + 2c − 1}h a=a/b; i true         (7)
         .              .
       a = 7e + 2, b = −11e − 3 ⊢ {b := 7ce + 2c − 1}h if (c>=a) a=a/b; i true               (6)
            .             .
         a = 7e + 2, b = −11e − 3 ⊢ {b := a · c − 1}h if (c>=a) a=a/b; i true                (5)
       .             .                      .
     a = 7e + 2, b = −11e − 3, d = 3e + 1 ⊢ h b=a*c-1; if (c>=a) a=a/b; i true               (4)
                .              .
           3a = 7d − 1, b = −2a + d ⊢ h b=a*c-1; if (c>=a) a=a/b; i true                     (3)
                      .
                  7b = −11a + 1 ⊢ h b=a*c-1; if (c>=a) a=a/b; i true                         (2)
                                .
                   11a + 7b = 1 ⊢ h b=a*c-1; if (c>=a) a=a/b; i true                         (1)


                         Fig. 1. Proof tree for the introductory example


                                                                             .
paper is permanently applied on the path condition (in (1), 11a + 7b = 1) and
the symbolic variable assignment (in (1), the identity).
     The complete proof is shown in Fig. 1. As first step, all formulas are nor-
malised: we choose an arbitrary well-ordering <r on the variables in the problem
(a <r b <r c) and move big variables to the left and small variables to the right
                   . . .
of the relations =, ≤, ≥, resulting in (2). We then concentrate on the equation
in (2), in order to (eventually) turn the leading coefficient 7 into a 1, by means of
the extended Euclidian algorithm (cf. [5]). A basis transformation is performed
that replaces b with a fresh variable d (such that a <r b <r c <r d). One can min-
                                             .
imise the coefficient of 11a by choosing b = −2a + d and replace the occurrence
of b in the original equation with −2a + d (afterwards, the equation is again
normalised, sequent (3)). Because the leading coefficient of the first equation is
still not 1, a second basis transformation a → 2d + e is performed (with d <r e).
This turns the leading coefficients of all equations into 1 (sequent (4)).
                                             .
     We can now leave out the equation d = 3e + 1, because d does not occur in
the sequent anymore. No further inferences are possible in the path condition
and the first statement of the program is executed, updating the variable as-
signment accordingly (for simplicity, we assume that no overflows are possible).
The assignment b := 7ce + 2c − 1 is written in front of the program in (5) and
is rewritten and simplified using the equations in (6). The next program state-
                                                      .                      .
ment causes the proof to split on the condition c ≥ a. One branch (c < a) can
immediately be closed because the program contains .no further statements. On
the other branch (7), we obtain a new assumption c ≥ a that can be simplified.
     The execution of the last assignment yields a new proof obligation (8) in
order to prevent division by zero. We prove by contradiction and normalise the
182      Philipp Rümmer


new equation in (9) (and also leave out the first two equations, which are no
longer needed for the proof). Because all other possibilities fail in the resulting
situation, a case split on the sign of one of the “independent”. variables c or e
                                                                            .
is .performed. Here, we will choose c and consider the cases c ≤ −1, c = 0, and
                    .                     .
c ≥ 1. The case c = 0 contradicts 7ce = −2c + 1, and the other two cases can be
handled in essentially the same way, so we show only the first one in (10).
                                                                               .
     By transitivity, from the two inequalities in (10) the inequality 7e + 2 ≤ −1
                                            .
can be derived, which is rounded to e ≤ −1 in (11). No further linear inference
steps are possible, but we can at this . point deduce  .
                                                           properties of product ce
by cross-multiplying
               .
                        the inequalities e  ≤ −1 and c ≤   −1, which yields the new
inequality 0 ≤ (−c − 1) · (−e − 1) in (12). After multiplying this inequality with
                                                         .
7, it can in (13) be rewritten using the equation 7ce = −2c + 1 and turned into
          .
−2c + 1 ≥ 7 · (−c − e − 1).
     Now, a. contradiction can.
                                be derived by reasoning
                                                  .
                                                           about linear inequalities.
                                                                                 .
From 5c ≥ −7e − 8 and c. ≤ −1 we derive 7e ≥ −3, which is rounded to e ≥ 0
and a contradiction to e ≤ −1.

2      Normalisation of Arithmetic Expressions
Before starting a derivation and permanently during a proof, our calculus nor-
malises (atomic) formulas. This was already demonstrated in the introductory
example, and in a proof tree we denote such simplification steps with simp.
We always fully expand polynomial expressions and represent them as a sum
of monomials α1 · m1 + · · · + αn · mn , in which α1 , . . . , αn are non-zero integer
literals and m1 , . . . , mn are pairwise distinct products of variables (possibly 1
as the empty product, and possibly 0 as the empty sum). Full expansion is in
general obviously a bad idea, but we found that it is a reasonable approach in
interactive Java program verification that in the vast majority of cases improves
the readability of formulas.

Sorting Terms. We put polynomial expressions into a canonical form by ordering
the factors in a monomial and the monomials in a polynomial. The ordering <r
that is used in both cases is a strict monomial ordering [6, 7]:
– We assume that a graded monomial ordering <r [6, 7] on products of vari-
  ables is given, i.e., a well-ordering (a total, well-founded ordering) with the
  properties: (i) deg m < deg m′ implies m <r m′ , and (ii) m <r m′ implies
  x · m <r x · m′ for all variables x. In practice, we define <r as a graded
  lexicographic ordering: we assume that a well-ordering <r on variables2 is
  given and then define c1 · · · cn <r d1 · · · dk if and only if n < k or n = k and
  {{c1 , . . . , cn }} <r {{d1 , . . . , dk }} (in the multiset extension of <r , cf. [9]).
2
    In reality, instead of variables we have to deal with arbitrary terms whose head-symbol is not +
    or ·, which are compared with a lexicographic path ordering [8].
                 A Sequent Calculus for Integer Arithmetic with Counterexample Generation          183


– We extend <r by constructing a well-ordering on integer literals: 0 <r 1 <r
  −1 <r 2 <r −2 <r 3 <r · · · .
– We extend <r on monomials by α · m <r α′ · m′ if and only if m <r m′ or
  m = m′ (modulo associativity and commutativity of ·) and α <r α′ .
– We extend <r on polynomials by α1 m1 + · · · + αn mn <r α1′ m′1 + · · · + αk′ m′k
  if and only if {{α1 m1 , . . . , αn mn }} <r {{α1′ m′1 , . . . , αn′ m′n }} (again using the
  multiset extension of <r ).
    For sake of brevity, we will also compare arbitrary terms with <r and im-
plicitly assume that the terms are first normalised.

Normalisation of .Formulas.     Atomic formulas are always written in the   form
                      . .                                   .             .
αs ∗ t with ∗ ∈ {≤, =, ≥}, employing equivalences like s < t ⇔ s + 1 ≤ t, and
transformed so that the left-hand side αs is the <r -greatest monomial of the
polynomial αs − t and α > 0. Furthermore, all inequalities are moved to the
antecedent, and in case αs − t is a constant polynomial an equation or inequality
is directly replaced with true or false.
    We always demand that the coefficients of non-constant terms in an equation
or inequality are coprime (do not have non-trivial factors in common), and oth-
erwise divide all coefficients by the greatest common divisor. This also detects
                         .
that equations like 2y. = 1 − 6c are unsolvable and equivalent to false,
                                                                    .
                                                                         and that
an inequality like 2y ≤ 1 − 6c can be simplified and rounded to y ≤ −3c thanks
to the discreteness of the integers.
    Finally, we add
                  .
                     a simple subsumption check for inequalities that eliminates
an. inequality s ≤ t from the antecedent in. case there is a second inequality
s ≤ t − β with β ≥ 0 (correspondingly for ≥).


3      Equation Handling: Gaussian Variable Elimination
In contrast to many decision procedures or SMT provers, equation and inequality
handling for integers are kept separate in our system. The initial reason for this
was that we believe that a reduction of equations to inequalities is not an option
for interactive proving. Much later we became aware that we also can design
more efficient, elegant and practical calculi for linear integer equations than for
inequalities, which afterwards justifies the decision. We believe that this is also
an important insight when working with the modular Java arithmetic, where
the handling of such equations is essential. The sequent calculus described in
this section is based on Gaussian elimination and the Euclidian algorithm.3 It
is complete, does not involve proof splitting, and is fast for all problems and
benchmarks that we so far have looked at.
3
    The calculus is in parts inspired by [5, Chapter 4.5.2], but in contrast to [5] we perform both row
    and column operations.
184      Philipp Rümmer


Row Operations. The primary rule of the calculus reduces an expression with
the help of an equation in the antecedent. The application of the rule is only
                                      .
allowed if s′ is not a subterm of s = t (u is an arbitrary term):4
         .
    Γ, s = t ⊢ φ[s′ + u · (s − t)], ∆
                .                      red
           Γ, s = t ⊢ φ[s′ ], ∆                if s′ + u · (s − t) <r s′
Example 1. We show how the rules red and simp are used to solve a system of
linear equations (with the ordering x <r y):
                          ∗
                .       .            .
             x = −5, y = −1 ⊢ x = −5
               .          .            .   red, simp
           3y = x + 2, y = −1 ⊢ x = −5
        .                          .         .    simp
    3y = x + 2, 5y − (3y − x − 2) = x ⊢ x = −5
               .            .          .          red
           3y = x + 2, 5y = x ⊢ x = −5
Column Operations. It is well-known that this kind of reduction alone does
not yield a complete calculus for integer equations. An example is the formula
            .
11a + 7b = 1 in the introductory example, for which no reduction steps are possi-
ble. To obtain a complete calculus, we also perform column operations—referring
to the usual matrix representation of the Gaussian elimination method. Assum-
ing that no more applications of red are possible in a sequent, and given an
               .
equation αx = s of the antecedent, we introduce a fresh unknown x′ and perform
a basis transformation x → u + x′ :
                     .      .
    Γ, α · (u + x′ ) = s, x = u + x′ ⊢ ∆
                       .                 col-red
               Γ, αx = s ⊢ ∆
                  if: x a variable, α > 1, (s − αu) = min<r {s − αu′ | u′ a term},
                      x′ a fresh variable, <r -smaller than all previous symbols
The term u is chosen such that the difference s − αu becomes <r -minimal. One
                                                                                .
subsequent application of simp will thus turn the new equation α(u + x′ ) = s
                    .
into a formula βy = t with β <r α. Likewise, βy is <r -smaller than the left-hand
sides of other equations β ′ y = t′ , because red was applied exhaustively prior to
col-red. This ensures the overall termination of the procedure (Lem. 1 below)
and allows to continue with reduction steps as long as linear equations are present
whose left-hand side has a non-unit-coefficient.
    We do not apply the rule col-red to nonlinear equations, due to the expe-
rience that the basis transformations performed by col-red cause more harm
than good in the nonlinear setting. This is because the usage of a good monomial
ordering <r becomes far more important than in the linear setting (col-red
effectively alters the ordering by introducing a new smallest variable, possibly
in a harmful way). We further discuss this issue in Sect. 5.
4
    In the rule, we write φ[s′ ] in the succedent to denote that the term s′ can occur in an arbitrary
    position in the sequent, in particular also in the antecedent.
             A Sequent Calculus for Integer Arithmetic with Counterexample Generation   185


Procedure 1. Apply simp with the highest priority, red with second-highest
priority, and col-red with the lowest priority.

Lemma 1. Procedure 1 terminates (for sequents containing arbitrary equations
and inequalities). For sequents that only contain linear equations, it is complete
and proof confluent.

Example 2. If a proof branch does not get closed by this procedure, the remain-
ing equations are an explicit description of all solutions (counterexamples) of
the equations:
       .                 .                    .            .
    x0 = 125x′′3 − 4, x1 = 25x′′3 − 1, x2 = 20x′′3 − 1, x3 = 16x′′3 − 1,
                             .               .                           ⊢
                         x′0 = 16x′′3 , x′3 = −3x′′3
                                         ..
                                          ..
                  .                .                 .
             x0 = 5x1 + 1, 4x1 = 5x2 + 1, 4x2 = 5x3 + 1 ⊢

The equations that define x′0 and x′3 can be removed afterwards, because these
symbols do not occur in the original problem and have no impact on its valid-
ity. A concrete counterexample is obtained by assigning arbitrary values to the
variables that only occur in the right-hand sides of equations (x′′3 ).


4    Handling of Linear Inequalities:
     Fourier-Motzkin Variable Elimination and Case Splits

Although Fourier-Motzkin variable elimination (cf. [10]) generally has a high
complexity, it is one of the most popular methods to handle linear inequalities
and used in proof assistants like PVS [11], Coq [12] or ACL2 [13, 14]. We found
Fourier-Motzkin to be a suitable base method both for linear and nonlinear in-
equality handling: most reasoning during verification is rather shallow and most
inequalities only share symbols with a small number of other inequalities (sparse
constraints), which is a situation where Fourier-Motzkin works well. At the same
time, the Fourier-Motzkin elimination rule is suited for interactive proving due
to its simplicity and the fact that it directly works on integers, in contrast to
more efficient linear programming techniques. The full procedure given in this
section is complete over the integers, but it involves proof splitting and does usu-
ally not terminate for invalid sequents, which means that it cannot (directly) be
used as a simplifier for interactive proving. We therefore also identify a subset
of the method that does not cause splitting and always terminates, but which
is no longer complete (which hardly ever matters in practice). An example for
a program that can be verified using the incomplete procedure (together with
axioms for division, modulo and Java arithmetic) is shown in Fig. 2.
186      Philipp Rümmer


The Incomplete Procedure. As equations have already been handled in the previ-
ous section, we can implement Fourier-Motzkin with a single rule for “cancelling”
two inequalities:
             .        .         .
      Γ, αs ≥ t, βs ≤ t′ , βt ≤ αt′ ⊢ ∆
                  .         .                 fm-elim
           Γ, αs ≥ t, βs ≤ t′ ⊢ ∆                              if α > 0, β > 0
                                    .
The resulting inequality βt ≤ αt′ does no longer contain the monomial s and is
therefore <r -smaller than both previous inequalities (after a subsequent appli-
cation of simp). To ensure termination, the rule must never be applied twice on
a proof branch to the same pair of inequalities.
    The performance of Fourier-Motzkin can be improved by adding a rule that
turns two inequalities into an equation, based on the law of anti-symmetry:
            .
      Γ, s = t ⊢ ∆
        .      .         anti-symm
   Γ, s ≤ t, s ≥ t ⊢ ∆
Procedure 2. Apply Procedure 1 (linear equations) with the highest priority,
the rule anti-symm with second highest priority and the rule fm-elim with
lowest priority.
Lemma 2. The procedure obtained in this way terminates when applied to a
sequent containing arbitrary equations and inequalities.

The Complete Procedure. Fourier-Motzkin is complete for rationals, but incom-
plete for integers. Our calculus is already more complete than pure Fourier-
Motzkin due to the normalisation from Sect. 2 (rounding of inequalities) and the
different equation handling of Procedure 1, which are enough to . handle many  .
cases that occur in practice (e.g., to show the inconsistency of 4x ≥ 5 ∧ 4x ≤ 7).
Making the calculus actually complete has therefore not been of great impor-
tance for us. The following approach to this end is rather simplistic, but it has
a counterexample generation property that is practically more relevant.
     Our calculus becomes complete by performing a systematic case analysis,
i.e., by doing proof splitting, in a way similar to Gomory’s cutting-planes (cf.
[10]). This is realised by the following rule for investigating the borderline case
of an inequality:
          .               .
     Γ, s < t ⊢ ∆ Γ, s = t ⊢ ∆
                  .                 strengthen
             Γ, s ≤ t ⊢ ∆
                                          .
There is a corresponding rule for ≥. The application of these rules does obviously
not terminate in general, but it does for valid sequents (of linear inequalities),
provided that a fair application strategy5 is used and the rule is combined with
5
    In the presence of subsumption checks (Sect. 2), we consider a strategy as fair if strengthen is
    eventually applied to each inequality or to any subsuming inequality.
                  A Sequent Calculus for Integer Arithmetic with Counterexample Generation         187

/*@
  @ normal_behavior
  @ requires -Decimal.PRECISION < f && f < Decimal.PRECISION
  @          && e + intPart < 32767 && -32768 < e + intPart;
  @ requires -Decimal.PRECISION < decPart && decPart < Decimal.PRECISION;
  @ modifiable intPart, decPart;
  @ ensures intPart * Decimal.PRECISION + decPart ==
  @         (\old(intPart) + e) * Decimal.PRECISION + \old(decPart) + f;
  @ ensures -Decimal.PRECISION < decPart && decPart < Decimal.PRECISION;
  @*/
publi void add(short e, short f) {
  intPart += e;
  if ( intPart > 0 && decPart < 0 ) {
    intPart--; decPart = (short)( decPart + PRECISION );
  } else if ( intPart < 0 && decPart > 0 ) {
    intPart++; decPart = (short)( decPart - PRECISION ); }
  decPart += f;
  if ( intPart > 0 && decPart < 0 ) {
    intPart--; decPart = (short)( decPart + PRECISION );
  } else if ( intPart < 0 && decPart > 0 ) {
    intPart++; decPart = (short)( decPart - PRECISION );
  } else {
    short retenue = 0; short signe = 1;
    if ( decPart < 0 ) {
      signe = -1; decPart = (short)( -decPart ); }
    retenue = (short)( decPart / PRECISION );
    decPart = (short)( decPart % PRECISION );
    retenue *= signe; decPart *= signe; intPart += retenue;
  } }

Fig. 2. Addition method of class Decimal taken from [15], where it was verified using the Loop tool
and PVS [11]. This method is part of the JavaCard Purse applet by Gemplus [16]. Using the KeY
implementation of our calculus, it takes about 200 seconds and 26000 rule applications to automatically
verify that the method adheres to its specification, reasoning about the modular arithmetic of Java.



Procedure 2. For an invalid sequent, a fair strategy eventually produces goals in
which all inequalities have been replaced with equations and where Procedure 1
can take over and produce a counterexample.
   Case distinctions are also necessary to handle equations in the succedent:
              .                    .
    Γ ⊢ s ≤ t, ∆ Γ ⊢ s ≥ t, ∆
                 .            split-eq
          Γ ⊢ s = t, ∆


Procedure 3. Apply Procedure 2 (the incomplete method) with the highest pri-
ority, the rule split-eq with second highest priority, and the rule strengthen
with lowest priority and in a fair manner.

Lemma 3. This procedure is complete and proof confluent, and it eventually
produces a counterexample for an invalid sequent.
188    Philipp Rümmer


Example 3. Consider the following example taken from [17]: Because Proce-
                                                                                .
dure 2 is not able to derive a contraction, we apply strengthen to x ≤ 2
                            .   .
and obtain two cases x = 1, x = 2 (thanks to anti-symm), the second of which
leads to a counterexample:
                                                    .           .
                     ∗                            y = 1, x = 2 ⊢
          .      .         .     fm-elim        .       .          .     anti-symm
        y ≥ 1, y ≤ 0, x = 1 ⊢                 y ≥ 1, y ≤ 1, x = 2 ⊢
                     ..                                     ..
                      ..                                     ..
      .            .          .             .             .            .
  4y ≥ x + 1, 4y ≤ x + 2, x = 1 ⊢        4y ≥ x + 1, 4y ≤ x + 2, x = 2 ⊢
                                     ..
                                      ..
                         .        .           .       .           strengthen
                 4y ≥ x + 1, 4y ≤ x + 2, x ≤ 2, x ≥ 1 ⊢

5     Handling of Nonlinear Polynomial Equations:
      Pseudo-Reduction and Gröbner Bases
The validity of equations or inequalities over arbitrary (possibly nonlinear) poly-
nomials over the integers is known to be undecidable [18]. This means that all
rules and procedures that we give from now on can never be complete and have
been employed or developed with the aim of handling the common cases: when
verifying programs, a large amount of the occurring nonlinear proof obligations
can and should be taken care of automatically by incomplete calculi. The most
important step to this end is to normalise nonlinear expressions (Sect. 2). We
describe a comparatively cheap extension—that does not cause any proof split-
ting and is suited for interactive proving—of Procedure 1 to deal with nonlinear
equation.
Pseudo-Reduction. As in Sect. 3, the primary rule for rewriting with (non-
linear) equations is red. Because we do not apply the rule col-red to non-
                                                                  .
linear equations, however, there are cases where equations αs = t with α > 1
remain
   .
          in. the antecedent that. cannot be simplified further. In the sequent
                      .
x ≥ 1, y ≥ 1, 2z 2 = y ⊢ xz 2 ≤ xy, for instance, none of the rules so far can
be applied. In order to handle such cases, we introduce a further reduction rule
that is based on pseudo-division and works by first multiplying the target ex-
                                                                         .
pression with a constant (cf. [5]). The rule must only be applied if αs = t and
       .
u · t = αt′ are different equations:
           .             .
   Γ, αs = t ⊢ φ[u · t = αt′ ], ∆
             .          .         pseudo-red
      Γ, αs = t ⊢ φ[s′ = t′ ], ∆                  if deg s > 1, α > 1, s′ = u · s
                                             .       .
There are similar rules for inequalities s′ ≤ t′ , s′ ≥ t′ . We apply pseudo-red
                                              .
only if the left-hand side of the equation αs = t is nonlinear and α > 1. Other-
wise, the normal reduction rule red can be used, possibly after turning α into
1 with help of col-red.
              A Sequent Calculus for Integer Arithmetic with Counterexample Generation   189


Gröbner Bases. Rewriting with nonlinear equations using the rules red and
pseudo-red is not confluent and is not able to decide ideal membership in a ring
of polynomials. Ideal membership is an approximation of semantic entailment
of (nonlinear) equations that we can practically decide: we complete the set of
antecedent equations by computing a Gröbner basis [6].
    The simplest way to generate a Gröbner basis is to saturate the antecedent
with “S-polynomial”-equations by considering all critical pairs of existing integer
equations—the Buchberger algorithm [6]. Our calculus produces a non-reduced
Gröbner basis over the field of rational numbers that only consists of polyno-
mial equations with integer coefficients, which are easier to compute and almost
as useful for reduction as actual Gröbner bases over the integers. Given two
equations with overlapping left-hand sides, S-polynomials are added as follows:
                                                           s = gcd(s, s′ ) · sr ,
         .       .              .                          s′ = gcd(s, s′ ) · s′r ,
    Γ, s = t, s′ = t′ , s′r · t = sr · t′ ⊢ ∆              0 < deg sr < deg s,
                 .          .                 s-poly
           Γ, s = t, s′ = t′ ⊢ ∆                           0 < deg s′r < deg s′
Similarly to the Fourier-Motzkin elimination rule, this rule must not be applied
repeatedly for the same pair of equations to ensure termination. The performance
of this naive implementation of Buchberger’s algorithm is not comparable with
more advanced methods, of course. We have yet to find, however, a verification
problem where this would be a problem.
Procedure 4. Apply Procedure 1 (linear equations) with highest priority, the
rule pseudo-red with second highest priority, the rule s-poly with third highest
priority, and Procedure 2 (linear inequalities) with lowest priority.
Lemma 4. Procedure 4 terminates when applied to a sequent containing arbi-
trary equations and inequalities.

6    Handling of Nonlinear Polynomial Inequalities:
     Cross-Multiplication and Case Splits
The handling of nonlinear polynomial inequalities is realised as an extension of
the linear inequality handling (Sect. 4). In order to apply linear reasoning to non-
linear arithmetic, we generate linear approximations of products and incremen-
tally strengthen the precision of the approximations through case distinctions.
Likewise, case splits are used to ensure the existence of linear approximations.
Our method has been developed as a heuristic, and we do not have an exact
description of the fragment of nonlinear arithmetic that it can handle. The main
application areas where the method has proven to be extremely useful are cor-
rectness proofs for lemma rules that can be loaded by the prover KeY [1], and
the verification of programs with the actual modular integer semantics of Java.
190      Philipp Rümmer


   Similarly to the approach in ACL2 [14, 19] (and using their terminology), the
primary rule to handle nonlinear inequalities is cross-multiplication:
           .       .       .
      Γ, s ≤ t, s′ ≤ t′ , 0 ≤ (t − s) · (t′ − s′ ) ⊢ ∆
                       .       .                         cross-mult
                  Γ, s ≤ t, s′ ≤ t′ ⊢ ∆
                                         .
There are corresponding rules for ≥ and for mixed pairs of inequalities. As usual
in order to ensure termination, cross-mult must not be applied repeatedly to
the same pair of inequalities.
    We can give. a geometric
                       .
                              interpretation of cross-multiplication: for two linear
inequalities x ≤ α, y ≤ β, cross-multiplication introduces a linear approximation
of the product (the bilinear term) xy. In this particular case, the right-hand side
                           .
of the new inequality xy ≥ βx + αy − αβ is the greatest.
                                                            plane
                                                              .
                                                                   that bounds the
expression xy from below (under the assumptions x ≤ α, y ≤ β). More generally,
the result of cross-multiplication is a bound on the value of a monomial in
terms of <r -smaller monomials. Deriving such bounds is, in practical cases,
often sufficient to prove statements in nonlinear arithmetic.

Restricting Cross-Multiplication. An unrestricted application of the rule cross-
mult can produce arbitrarily many inequalities and does not terminate. As a
heuristic, we only use cross-mult if the product s · s′ already occurs as a factor
within a left-hand side of an equation or inequality (ignoring the coefficient of
s · s′ ). Although this is not strong enough to ensure termination, it guarantees
that the total degree of occurring monomials is bounded. We found this heuristic
to work reasonably well for most cases (a counterexample is Ex. 5 below).

Case Splits. For two reasons, it is crucial to combine cross-multiplication with
case distinctions: (i) nonlinear monomials over the complete set of integers do
in general not have linear bounds (observe, for instance, that the term xy is not
bounded from above or below by any linear expression in x and y). (ii) case
distinctions are in general the only way to strengthen linear bounds (again,
                                                  .       .
consider the term xy under the assumptions x ≤ α, y ≤ β, for which no more
precise linear lower bound exists than βx + αy − αβ).
    To account for (i), we introduce a rule that splits over the sign of the value
of a term. We apply this rule for variables x that occur in the left-hand side of
equations or inequalities:
           .            .            .
      Γ, x < 0 ⊢ ∆ Γ, x = 0 ⊢ ∆ Γ, x > 0 ⊢ ∆
                                             sign-cases
                       Γ ⊢ ∆
                                                                     .
Ternary splits are motivated by the observation that the case x = 0 usually
is easy to handle (significantly easier than the original problem), while at the
             A Sequent Calculus for Integer Arithmetic with Counterexample Generation       191

                                    .
same time a strict inequality
                         .
                              x > 0 appears to be of much greater use in cross-
                                                          .
multiplication than x ≥ 0 (and correspondingly for x < 0). In our experience,
the rule sign-cases outperforms binary cuts.
    Point (ii) is accommodated by using the rule strengthen from Sect. 4,
which we apply to linear inequalities in order to incrementally restrict the domain
                                                                                .
of a variable.
      .
               For  the example above,   after strengthening  the inequality  x ≤ α
to x ≤ α − 1, we can also derive a better bound βx + (α − 1)y − αβ + β for the
value of xy.

Procedure 5. Apply Procedure 4 (equations handling and the incomplete proce-
dure for linear inequalities) with the highest priority, the rule split-eq with sec-
ond highest priority, and the rules cross-mult, sign-cases and strengthen
with the lowest priority and in a fair manner.

Example 4. We give three further examples that can be proven using Proce-
dure 5 (the last two ones are taken from [14, 19]). In practice, it can often be
observed that Procedure 5 is able to solve nonlinear equational problems that
cannot be proven using Procedure 4 (only using Gröbner bases).
       .       .      .               .                 .        .         .            .
    xy = 0 ⊢ x = 0, y = 0          x2 = 2 ⊢          0 < ab, 0 < cd, 0 < ac ⊢ 0 < bd

Example 5. A valid sequent that. is not provable
                                             .
                                                 due. to the restriction on the
                                                             .
application of cross-mult is ac ≤ bd − 1, de
                                          .
                                             ≤ a, c ≥. 1, ce = b ⊢ . The prob-
lem can be solved by cross-multiplying de ≤ a and c ≥ 1.

Lemma 5. When applied to an invalid sequent (containing arbitrary equations
and inequalities), Procedure 5 will eventually produce a counterexample.


7    Related Work
Most similar to our approach is the arithmetic handling in ACL2 [13, 14], which
also employs Fourier-Motzkin for linear and cross-multiplication for nonlinear
arithmetic. Concerning differences, ACL2 runs arithmetic handling as a purely
automated procedure, supports also rationals, does not have separate procedures
for equations and does not seem to perform a systematic case analysis.
    An method for handling linear equations and inequalities similar to our ap-
proach (but lacking counterexample generation) is described in [17] and imple-
mented in the Tecton tool. Related is also [20] about the extension of linear
reasoning to nonlinear reasoning.
    Higher-order proof assistants usually support integer arithmetic and are so
general that arbitrary procedures can be implemented on top of them, often
targeting mathematical proofs. In comparison, we tried to develop a simple cal-
culus/procedure specifically for Java verification that works “out of the box”
192    Philipp Rümmer


and requires little expertise. The PVS proof assistant [11] can handle linear
integer arithmetic and can simplify nonlinear expressions (involving multiplica-
tion and division) to some degree, but does (apparently) not go as far as our
approach or ACL2. The Coq system [12] implements an incomplete version of
the Omega method for deciding Presburger arithmetic (linear integer arithmetic
with quantifiers) that essentially boils down to Fourier-Motzkin. Coq can also
simplify ring expressions like polynomials. For HOL light [21], a number of tac-
tics and decision procedures for arithmetic have been implemented, including
Cooper’s method for deciding Presburger arithmetic, handling of congruences
and simplification of polynomial expressions.
    Linear arithmetic is one of the most important theories supported by SMT
solvers (which generally provide incomparably better performance for linear
arithmetic than our implementation based on a general theorem prover frame-
work), see [22] for a list. To the best of our knowledge, no SMT solver offers
support for nonlinear arithmetic similar to our approach or ACL2. SMT solvers
typically use linear programming techniques like Simplex, combined with meth-
ods like branch-and-bound or Gomory’s cutting planes to realise completeness
on the integers.

8     Conclusions and Future Work
We have presented the main components of a proof procedure for linear and
nonlinear integer arithmetic, represented as sequent calculus rules together with
application strategies. The procedure is completely implemented, and the sound-
ness of the implementation is verified in the prover KeY itself. In addition to
the calculus shown here, KeY also supports division and modulo operations and
provides further methods like polynomial division. Based on this, we have for-
malised the Java semantics of integer operations.
    For the future, we are considering a more efficient stand-alone implemen-
tation of the calculus, possibly based on the DPLL(T) framework. As a more
conceptual extension, we plan to combine the calculus with free-variable rea-
soning for handling quantifiers. The general approach for this is described in
[23], but needs to be investigated more carefully. Finally, we would like to add
support for bit-wise operations (as they can be found in Java).

Acknowledgements. I want to thank Wolfgang Ahrendt and Richard Bubel for
many inspiring discussions and comments on this paper. Thanks are also due to
the anonymous referees for helpful comments.

References
1. Beckert, B., Hähnle, R., Schmitt, P.H., eds.: Verification of Object-Oriented Software: The KeY
   Approach. LNCS 4334. Springer-Verlag (2007)
                A Sequent Calculus for Integer Arithmetic with Counterexample Generation             193


 2. Mostowski, W.: Fully verified JavaCard API reference implementation. In: 4th International
    Verification Workshop. (2007) To appear.
 3. Fitting, M.C.: First-Order Logic and Automated Theorem Proving. 2nd edn. Springer-Verlag,
    New York (1996)
 4. King, J.C.: Symbolic execution and program testing. Communications of the ACM 19 (1976)
    385–394
 5. Knuth, D.E.: The Art of Computer Programming: Seminumerical Algorithms. Addison-Wesley
    (1997) Third edition.
 6. Buchberger, B.: An algorithmical criterion for the solvability of algebraic systems. Aequationes
    Mathematicae 4 (1970) 374–383 (German).
 7. Buchberger, B.: A critical-pair/completion algorithm for finitely generated ideals in rings. In: Pro-
    ceedings of the Symposium ”Rekursive Kombinatorik” on Logic and Machines: Decision Problems
    and Complexity, London, UK, Springer-Verlag (1984) 137–161
 8. Dershowitz, N.: Termination of rewriting. J. Symb. Comput. 3 (1987) 69–116
 9. Dershowitz, N., Manna, Z.: Proving termination with multiset orderings. Commun. ACM 22
    (1979) 465–476
10. Schrijver, A.: Theory of Linear and Integer Programming. Wiley (1986)
11. Owre, S., Rajan, S., Rushby, J., Shankar, N., Srivas, M.: PVS: Combining specification, proof
    checking, and model checking. In Alur, R., Henzinger, T.A., eds.: Proceedings, CAV. Volume
    1102 of LNCS., Springer (1996) 411–414
12. Dowek, G., Felty, A., Herbelin, H., Huet, G., Murthy, C., Parent, C., Paulin-Mohring, C., Werner,
    B.: The Coq proof assistant user’s guide. Rapport Techniques 154, INRIA, Rocquencourt, France
    (1993) Version 5.8.
13. Kaufmann, M., Moore, J.S.: ACL2: An industrial strength version of nqthm. In: Compass’96:
    Eleventh Annual Conference on Computer Assurance, Gaithersburg, Maryland, National Institute
    of Standards and Technology (1996)
14. Warren A. Hunt, J., Krug, R.B., Moore, J.S.: Linear and nonlinear arithmetic in ACL2. In Geist,
    D., Tronci, E., eds.: CHARME. Volume 2860 of Lecture Notes in Computer Science., Springer
    (2003) 319–333
15. Breunesse, C.B., Jacobs, B., van den Berg, J.: Specifying and verifying a decimal representa-
    tion in java for smart cards. In: Proceedings of the 9th International Conference on Algebraic
    Methodology and Software Technology, London, UK, Springer-Verlag (2002) 304–318
16. : Gemplus purse applet. (http://www.gemplus.com/smart/r d/publications/case-study/)
17. Kapur, D., Nie, X.: Reasoning about numbers in tecton. In: International Symposium on Method-
    ologies for Intelligent Systems, Charlotte, North Carolina. (1994)
18. Matijasevic, Y.: Enumerable sets are diophantine (Russian). Dokl. Akad. Nauk SSSR 191 (1970)
    279–282 Translation in Soviet Math Doklady, Vol 11, 1970.
19. Warren A. Hunt, J., Krug, R.B., Moore, J.S.: Integrating nonlinear arithmetic into into ACL2. In:
    Fifth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2004).
    (2004)
20. Kapur, D., Cyrluk, D.: Reasoning about nonlinear inequality constraints: a multi-level approach.
    In: Proceedings of a workshop on Image understanding workshop, San Francisco, CA, USA,
    Morgan Kaufmann Publishers Inc. (1989) 904–915
21. Harrison, J.: The HOL light manual (1.1) (2000)
22. Ranise, S., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org
    (2006)
23. Rümmer, P., Shah, M.A.: Proving programs incorrect using a sequent calculus for Java Dynamic
    Logic. In: International Conference on Tests And Proofs (TAP). LNCS, Springer (2007) To
    appear.


A      Proofs (-Sketches)
Proof. (Lem. 1) Termination: the termination of simp and red is immediate.
                                             .
We call the left-hand sides x of equations x = s (x a variable) in the antecedent
194      Philipp Rümmer


“defined variables,” and all other variables “independent variables.” When ap-
plying red exhaustively, each defined variable will eventually occur in exactly
one place in the sequent (namely, in the defining equation).
    For proving termination when col-red is added, we show that the leading
                                      .
coefficients α > 1 of equations αx = s constantly get smaller. We introduce a
well-founded ordering on the set of multisets over                 N
                                                             ∪ {∞} by lexicographic
comparison: for a1 ≤ · · · ≤ an , b1 ≤ · · · ≤ bm , we define:

      {{a1 , . . . , an }} <m {{b1 , . . . , bm }} iff
                                   n < m or (n = m and (a1 , . . . , an ) <lex (b1 , . . . , bm ))

For a sequent and an independent variable x, we then consider the divisors
                        N
gcd(α1 , . . . , αn ) ∈ ∪ {∞}, where α1 , . . . , αn are all coefficients of equations
      .
αi x = si in the antecedent (we define gcd() = ∞). The multiset of such gcds for
all independent variables gets <m -smaller for each application of col-red, and
it gets <m -smaller or stays the same when red is applied (each time potentially
followed by an application of simp). This proves termination.
    Completeness and proof confluence: assume that no further rules can be ap-
plied, but the proof branch at hand is not closed. This implies that the coefficient
of the left-hand side of all equations is 1 (otherwise, simp or col-red can be
applied), and that no left-hand side term occurs in two places in the sequent (oth-
erwise, red can be applied). Due to the fact that 0 is the only polynomial whose
value is constantly 0 (and correspondingly for tuples of polynomials), there is a
countermodel for the equations in the succedent (a valuation of the independent
variables). We extend this valuation on the defined variables according to the
equations in the antecedent. When investigating red and col-red, it can be
seen that this countermodel also is a countermodel of the original sequent.

Proof. (Lem. 2) To see that the application of fm-elim terminates, consider
the multiset of pairs of inequalities in the antecedent to which fm-elim can but
has not yet been applied. Pairs of inequalities can be compared lexicographically
using <r , and multisets of pairs can be compared using the multiset extension
of this ordering. As the multiset gets smaller in this well-founded ordering each
time fm-elim is applied, termination is guaranteed.
    The rule anti-symm can introduce new equations. Such a new equation is
either trivially true and is eliminated, or it is a contradiction and the proof
branch is closed, or it reduces the number of independent variables by one. In
the last case, Fourier-Motzkin basically has to start over once Procedure 1 has
done its job, but this can only happen a finite number of times.

</pre>