We study and implement concrete methods for the verification of both imperative as well as functional programs in the frame of the Theorema system. The distinctive features of our approach consist in the automatic generation of loop invariants (by using combinatorial and algebraic techniques), and the generation of verification conditions as first-order logical formulae which do not refer to a specific model of computation.

Combining Karatsuba multiplication with a technique developed by Krandick for computing the high-order part of the quotient, we obtain an integer division algorithm which is only two times slower, on average, than Karatsuba multiplication. The main idea is to delay part of the dividend update until this can be done by multiplication between large balanced operands. An implementation under saclib is faster than classical multiplication at 40 words, and becomes two times faster at 250 words. Introduction The Karatsuba method for long integer multiplication [4] is probably the only asymptotically fast algorithm of practical use for integer arithmetic. Depending on the implementation, the break-even point against the classical algorithm is typically between 5 and 50 words. However, integer division with remainder does not benefit from this algorithm. Indeed, although theoretically division has the same time complexity as multiplication (see e.g. [5], p. 275), a division algorithm designe...

We design a systolic coprocessor for the addition of signed normalized rational numbers. This is the most complicated rational operation: it involves GCD, exact division, multiplication and addition/subtraction. In particular the implementation of GCD and exact division improve significantly (2 to 4 times) previously known solutions. In contrast to the traditional approach, all operations are performed least-significant digits first. This allows bit-pipelining between partial operations at reduced area-cost. An Atmel FPGA design for 8-bit operands consumes 730 cells (3,500 equivalent gates) and runs at 25 MHz (5 MHz after layout). For 32-bit operands this would be in the same timing range as the software solutions, however a significant speed-up can be expected for longer operands because the linear time-complexity of the hardware algorithms.

We improve the classical result of Brent and Kung (1985) by a factor of 12 in area consumption, while maintaining the same average running time. Global broadcasting is eliminated using a novel technique which is more efficient then Leisersons (1982) semisystolic-to-systolic transformation and can be also applied to other arithmetic algorithms. Experiments using field programmable gate arrays demonstrate the possibility of speeding-up long integer arithmetic by two orders of magnitude by implementing this algorithm in dedicated hardware.>

The execution times of several algorithms for computing the GCD of arbitrary precision integers are compared. These algorithms are the known ones (Euclidean, binary, plus-minus), and the improved variants of these for multidigit computation (Lehmer and similar), as well as new algorithms introduced by the author: an improved Lehmer algorithm using two digits in partial consequence computation, and a generation of the binary algorithm using a new concept of modular conjugates. The last two algorithms prove to be the fastest of all, giving a speedup of six to eight times over the classical Euclidean scheme, and two times over the best currently known algorithms. Also, the generalized binary algorithm is suitable for systolic parallelization in a least-significant digits first pipelined manner.>

The authors present a systolic algorithm for normalization of rational numbers which is scalable to arbitrary length operands, and they discuss the possibility of implementing it within a rational arithmetic coprocessor for the use of computer algebra systems. A preliminary estimation shows that the performance for 32 bit operands is comparable to that of a fast RISC processor, but for long operands (e.g., 50 words) a significant speed-up (50 times) can be achieved.>

A generalization of the binary algorithm for operation at 'word level" by using a new concept of 'modular conjugates" computes the GCD of multiprecision integers two times faster than Lehmer-Euclid method.Most importantly, however, the new algorithm is suitable for systolic parallelization, in 'least-significant digits jirst" pipelined manner and for aggregation with other systolic algorithms for the arithmetic of multiprecision rational numbers.