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 interactive 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 (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 theorem provers (which are, nevertheless, extremely useful for dealing with simpler proof obligations). As a complementary approach, we have developed a novel calculus 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 notation. 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 polynomials (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 inequalities, prevents case splits and guarantees termination (Procedure 4 in Sect. 5), and (ii) for proving and countermodel construction, which enables all parts (Procedure 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 ⊢ b=a*c-1; if (c>=a) a=a/b; true(1)

In Java dynamic logic, this sequent expresses that the program in angle brackets terminates normally, i.e., in particular does not raise exceptions, given the assumption 11a + 7b . = 1. A proof is conducted by rewriting the program following the symbolic execution paradigm [4], whereby the calculus presented in this

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

(

(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 normalised: 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 minimise 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 assignment 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 statement 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 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 = −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

Normalisation of Arithmetic Expressions

Before starting a derivation and permanently during a proof, our calculus normalises (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 • m 1 + • • • + α n • m n ,

in which α 1 , . . . , α n are non-zero integer literals and m 1 , . . . , m n 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 variables 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

c 1 • • • c n < r d 1 • • • d k if and only if n < k or n = k and {{c 1 , . . . , c n }} < r {{d 1 , . . . , d k }} (in the multiset extension of < r , cf. [9]

).

-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 m 1 + • • • + α n m n < r α ′ 1 m ′ 1 + • • • + α ′ k m ′ k if and only if {{α 1 m 1 , . . . , α n m n }} < 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 implicitly assume that the terms are first normalised. ≤ 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 otherwise 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 . ≥).

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.

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)], ∆ Γ, s . = t ⊢ φ[s ′ ], ∆ red 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 3y . = x + 2, y . = −1 ⊢ x . = −5 red, simp 3y . = x + 2, 5y − (3y − x − 2) . = x ⊢ x . = −5 simp 3y . = x + 2, 5y . = x ⊢ x . = −5 red

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 possible. To obtain a complete calculus, we also perform column operations-referring to the usual matrix representation of the Gaussian elimination method. Assuming 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 ′ ⊢ ∆ Γ, αx . = s ⊢ ∆ col-red 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 experience 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.

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 remaining equations are an explicit description of all solutions (counterexamples) of the equations:

x 0 . = 125x ′′ 3 − 4, x 1 . = 25x ′′ 3 − 1, x 2 . = 20x ′′ 3 − 1, x 3 . = 16x ′′ 3 − 1, x ′ 0 . = 16x ′′ 3 , x ′ 3 . = −3x ′′ 3 ⊢ . . . . x 0 . = 5x 1 + 1, 4x 1 . = 5x 2 + 1, 4x 2 . = 5x 3 + 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 validity. A concrete counterexample is obtained by assigning arbitrary values to the variables that only occur in the right-hand sides of equations (x ′′ 3 ).

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 inequality 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 usually 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.

The Incomplete Procedure. As equations have already been handled in the previous section, we can implement Fourier-Motzkin with a single rule for "cancelling" two inequalities:

Γ, αs . ≥ t, βs . ≤ t ′ , βt . ≤ αt ′ ⊢ ∆ Γ, αs . ≥ t, βs . ≤ t ′ ⊢ ∆ fm-elim 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 application 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 ⊢ ∆ Γ, s . ≤ t, s . ≥ t ⊢ ∆ anti-symm 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 incomplete 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 importance 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 ⊢ ∆ Γ, s .

≤ t ⊢ ∆ strengthen

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 strategy 5 is used and the rule is combined with /*@ @ ÒÓÖÑ Ð Ú ÓÖ @ Ö ÕÙ Ö × -Decimal.PRECISION < f && f < Decimal.PRECISION @ && e + intPart < 32767 && -32768 < e + intPart; @ Ö ÕÙ Ö × -Decimal.PRECISION < decPart && decPart < Decimal.PRECISION; @ ÑÓ Ð intPart, decPart; @ Ò×ÙÖ × intPart * Decimal.PRECISION + decPart == @ ( ÓÐ (intPart) + e) * Decimal.PRECISION + ÓÐ (decPart) + f; @ Ò×ÙÖ × -Decimal.PRECISION < decPart && decPart < Decimal.PRECISION;

@*/ ÔÙ Ð ÚÓ add(× ÓÖØ e, × ÓÖØ f) { intPart += e; ( intPart > 0 && decPart < 0 ) { intPart--; decPart = (× ÓÖØ)( decPart + PRECISION ); } Ð× ( intPart < 0 && decPart > 0 ) { intPart++; decPart = (× ÓÖØ)( decPart -PRECISION ); } decPart += f; ( intPart > 0 && decPart < 0 ) { intPart--; decPart = (× ÓÖØ)( decPart + PRECISION ); } Ð× ( intPart < 0 && decPart > 0 ) { intPart++; decPart = (× ÓÖØ)( decPart -PRECISION ); } Ð× { × ÓÖØ retenue = 0; × ÓÖØ signe = 1; ( decPart < 0 ) { signe = -1; decPart = (× ÓÖØ)( -decPart ); } retenue = (× ÓÖØ)( decPart / PRECISION ); decPart = (× ÓÖØ)( 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, ∆ Γ ⊢ s . = t, ∆ split-eq Procedure 3.

Apply Procedure 2 (the incomplete method) with the highest priority, 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.

Example 3. Consider the following example taken from [17]: Because Procedure 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, y . ≤ 0, x . = 1 ⊢ fm-elim . . . . 4y . ≥ x + 1, 4y . ≤ x + 2, x . = 1 ⊢ y . = 1, x . = 2 ⊢ y . ≥ 1, y . ≤ 1, x . = 2 ⊢ anti-symm . . . . 4y . ≥ x + 1, 4y . ≤ x + 2, x . = 2 ⊢ . . . . 4y . ≥ x + 1, 4y . ≤ x + 2, x . ≤ 2, x . ≥ 1 ⊢ strengthen

Handling of Nonlinear Polynomial Equations: Pseudo-Reduction and Gröbner Bases

The validity of equations or inequalities over arbitrary (possibly nonlinear) polynomials 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 splitting 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 (nonlinear) equations is red. Because we do not apply the rule col-red to nonlinear 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 expression 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 ′ ], ∆ Γ, αs . = t ⊢ φ[s ′ . = t ′ ], ∆ pseudo-red 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. Otherwise, the normal reduction rule red can be used, possibly after turning α into 1 with help of col-red.

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 polynomial 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 . = t, s ′ . = t ′ , s ′ r • t . = s r • t ′ ⊢ ∆ Γ, s . = t, s ′ . = t ′ ⊢ ∆ s-poly s = gcd(s, s ′ ) • s r , s ′ = gcd(s, s ′ ) • s ′ r , 0 < deg s r < deg s, 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 arbitrary equations and inequalities.

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 nonlinear arithmetic, we generate linear approximations of products and incrementally 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 correctness 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.

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 ′ ) ⊢ ∆ Γ, s . ≤ t, s ′ . ≤ t ′ ⊢ ∆ cross-mult

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 crossmult 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 same time a strict inequality x . > 0 appears to be of much greater use in crossmultiplication 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 procedure for linear inequalities) with the highest priority, the rule split-eq with second 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 Procedure 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). Lemma 5. When applied to an invalid sequent (containing arbitrary equations and inequalities), Procedure 5 will eventually produce a counterexample.

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 approach (but lacking counterexample generation) is described in [17] and implemented 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 calculus/procedure specifically for Java verification that works "out of the box" and requires little expertise. The PVS proof assistant [11] can handle linear integer arithmetic and can simplify nonlinear expressions (involving multiplication 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 tactics 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 framework), 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 methods like branch-and-bound or Gomory's cutting planes to realise completeness on the integers.

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 soundness 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 formalised the Java semantics of integer operations.

For the future, we are considering a more efficient stand-alone implementation of the calculus, possibly based on the DPLL(T) framework. As a more conceptual extension, we plan to combine the calculus with free-variable reasoning 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).

"defined variables," and all other variables "independent variables." When applying 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 . For a sequent and an independent variable x, we then consider the divisors gcd(α 1 , . . . , α n ) ∈ AE ∪ {∞}, where α 1 , . . . , α n are all coefficients of equations α i x . = s i 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 applied, 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 (otherwise, 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.