“The Tokeneer project is a milestone in the transfer of program verification technology into industrial application. Publication of the full documents for the project has provided unprecedented experimental material for yet further development of the technology by pure academic research. It will serve as a touchstone to chart and measure progress of the basic science of programming, on which the technology is based.”

Sir Tony Hoare FRS

“The publication by Praxis and NSA of the Tokeneer system is a fantastic contribution to the software engineering research and teaching community. Good case studies have been very hard to find, and have often been proprietary. Finally, we have a full and open example of a development from a world leader in high integrity systems with exemplary requirements, specifications, design and code. I’m very excited about the impact this might have in our field, in both teaching and research, and the potential it might have in moving us towards a more open community with greater collaboration between industry and academia, and a more constructive engagement of theory and practice.”

Professor Daniel Jackson
MIT Computer Science Lab

“The availability of the Tokeneer results in this form will stimulate researchers working on the Grand Challenge of software verification – it is particularly apt that it comes from Praxis who have used formal methods in order to achieve high quality results even when not required to do so by certifiers.

I particularly welcome the approach taken by Praxis’ engineers that they use a variety of formal and semi-formal methods to fit the task in hand.”

Professor Cliff Jones
University of Newcastle

“I am delighted that the Tokeneer material has been made freely available. The Tokeneer project shows that highly dependable software can be developed cost-effectively and that strong software engineering methods are mature and easily taught to software developers in industry.

Now that Praxis and the NSA have made the full project documents available, any company can work through the project, experiment with the methods, and convince themselves that near-zero-defect software is a commercial reality.

The project will also be of great benefit to academics, as SPARK and Tokeneer provide a benchmark against which they can measure the advantages of their latest research tools and methods.

Praxis and the NSA have thrown down a challenge to industry. If you cannot develop software this dependably and cost-effectively, you need to catch up – or to give up!”

Martyn Thomas CBE FREng
Visiting Professor of Software Engineering
Oxford University Computing Laboratory