**Go backward to** Applying Larch/C++ to the STL

*Gary Leavens*

**Go up to** Specification and Verification

**Go forward to** Language Independent Container Specification

*Alexandre Zamulin*

*Mizar* Verification of Generic Algebraic Algorithms

*Christoph Schwarzweller*

We propose the *Mizar* system as a theorem prover capable of
verifying generic algebraic algorithms on an appropriate abstract
level. The main advantage of the *Mizar* theorem prover is its
special input language that enables textbook-style presentation of
proofs, hence proofs in the language of algebra. Using *Mizar* we
were able to give a rigorous machine-assisted correctness proof of a
generic version of Brown/Henrici arithmetic in the field of quotients
over arbitrary gcd domains. In this talk we give a short introduction
into the *Mizar* language and show how to use the system to verify
generic algebraic algorithms. We also deal with proof documentation
based on literate programming, claiming that even complex proofs can be
presented so that they stay readable and understandable.