Praxis High Integrity Systems, Ltd.
20 Manvers Street
Bath, BA1 1PX
Phone: +44 (0)1225 466991
FAX: +44 (0)1225 469006
Email: sparkinfo at praxis-his.com
URL: www.praxis-his.com
and www.sparkada.com
Praxis High Integrity Systems specializes in the development of highly-critical, software intensive systems and related consultancy, including independent verification and validation. We make use of the most advanced tools and techniques available including formal methods and software proof. Although mainly a services company, we also produce and support tools where these have a proven value in the development of critical systems. Our SPARK language provides unparalleled support for formal reasoning about software systems. It has exact, unambiguous semantics while remaining compatible with mainstream Ada development tools. Its support tool, the SPARK Examiner, provides a range of analysis options including a rigorous demonstration that code is "exception free" under all circumstances. SPARK has a proven track record in facilitating high quality at low cost to the most exacting standards such as DO-178B, Def Stan 00-55 and Common Criteria. SPARK is a good example of the "pragmatic formalism" that characterizes the company.