JSA Research & Innovation

Automated proof of program correctness

The SPARK programming language allows development of software with automatically generated proofs that they don't contain any run-time errors, and that the properties described in the source text always will be fulfilled.

I have published a few examples of SPARK 2014 source text:

Please call or write if you are interested in development of SPARK 2014 software.

If you have questions or requests, please send them to <services@jacob-sparre.dk>, or call +45 21 49 08 04.

PortfolioCurriculum vitaePublication listProductsServicesScienceRSS feedsCalendar

JSA Research & Innovation • Jægerparken 5, 2. th. • 2970 Hørsholm • Danmark