Monday 7 April 2008

David says: Thank you for your response to our request in January. We are still open to minor suggestions from our existing users, but we have now withdrawn the survey form. Please email us using the address that (as an existing user) you will already have.

Thursday 31 January 2008

David says: This is intended to be a major release, and planned changes to the theorem prover are already under way. At this time we are open to suggestions from our existing users as to what else they would find helpful.

Tuesday 29 January 2008

Yet more improvements to the theorem prover! Plus some enhancements to the tool:

• Loop variants can now be specified as '?' without code generation or verification being refused.
• The amount of text in the Output box of the Project Manager can now exceed 32K characters even under older versions of Windows.
• Files builtin.pd and rubric.pd now contain version numbers, which are shown in proof output.
• HTML output now uses CSS and declares a DOCTYPE.
• When a proof fails, the verifier will sometimes generate a suggestion for how to fix the specification.
• Error and warning messages in the Output window are now highlighted

Friday 28 September 2007

Our paper on mathematical verification of C programs was presented at SEFM in September 2007. If you missed it, read the paper here...

Friday 13 January 2006

We're proud to announce the involvement of Escher Technologies with this challenge. Full article here