Praxis Critical Systems

Rod Chapman

Praxis Critical Systems
Roderick Chapman
Praxis Critical Systems Limited
20 Manvers Street, Bath BA1 1PX, UK

Phone: +44 1225 466991
FAX: +44 1225 469006

Praxis Critical Systems

Praxis Critical 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.