Date: Tue, 21 Jan 2003 11:49:37 -0600 (CST) From: "Erik H. Reeber" Hello everyone, This week I will talk about the work of Praxis Critical Systems. Praxis Critical Systems is a British company that specializes in high-integrity systems. Their approach will not be entirely satisfying to everyone as they still rely a great deal on hand-proofs for certain systems and, in other systems, they do very few proofs at all. However, I think it's interesting to see how this company develops high-integrity software. Furthermore, their tools are interesting in their own right. They have developed their own language (SPARK -- a precise subset of Ada), simplifier, and proof-checker. I am preparing a one-hour presentation, based on a bunch of their papers. My talk may go longer if we have the usual amount of discussion. -Erik