Buy article online - an online subscription or single-article purchase is required to access this article.
Download citation
Download citation
link to html
An application of formal verification (using the proof assistant Isabelle/HOL) for ensuring the correctness of scientific data processing software in the crystallographic domain is presented. The proposed process consists of writing a pseudocode that describes an algorithm in a succinct but mathematically unambiguous way, then formulating or reusing necessary Isabelle theories and proving algorithm properties within these theories, and finally implementing the algorithm in a practical programming language. Both the formal proof and the semi-formal algorithm analysis are demonstrated on an example of a simple but important algorithm (widely used in crystallographic computing) that reconstructs a space-group operator list from a subset of symmetry operators. The cod-tools software package that implements the verified algorithm is also presented. On the basis of the reported results, it is argued that broader application of formal methods (e.g. formal verification of algorithm correctness) allows developers to improve the reliability of scientific software. Moreover, the formalized (within the proof assistant) domain-specific theory can be reused and gradually extended, thus continuously increasing the automation level of formal algorithm verification.

Supporting information


Zip compressed file
Machine-readable sources of the Isabelle/HOL proof of the correctness of the optimized and initial versions of the simple space-group-builder (core) algorithm SimpleBuilderInitial.


Zip compressed file
The code used to generate Table 1 and to test implementations of both the initial and optimized algorithms.

Subscribe to Journal of Applied Crystallography

The full text of this article is available to subscribers to the journal.

If you have already registered and are using a computer listed in your registration details, please email for assistance.

Buy online

You may purchase this article in PDF and/or HTML formats. For purchasers in the European Community who do not have a VAT number, VAT will be added at the local rate. Payments to the IUCr are handled by WorldPay, who will accept payment by credit card in several currencies. To purchase the article, please complete the form below (fields marked * are required), and then click on `Continue'.
E-mail address* 
Repeat e-mail address* 
(for error checking) 

Format*   PDF (US $40)
   HTML (US $40)
   PDF+HTML (US $50)
In order for VAT to be shown for your country javascript needs to be enabled.

VAT number 
(non-UK EC countries only) 

Terms and conditions of use
Contact us

Follow J. Appl. Cryst.
Sign up for e-alerts
Follow J. Appl. Cryst. on Twitter
Follow us on facebook
Sign up for RSS feeds