Escher Technologies researches, develops and delivers tools for the efficient construction of provably correct software. Using advanced Automated Reasoning technology, Perfect Developer and the Escher C Verifier reduce the cost of developing safety-critical software or software for other high-integrity applications. For universities and colleges which offer courses in formal methods of software development: Perfect Developer Free Edition makes this challenging subject easier to teach and enjoyable to learn.
Perfect Developer is a tool for specifying and modeling software systems, providing formal proofs of correctness. Optionally, code can be generated from the model, in a choice of languages.
Functional specifications can be expressed at a high level and refined to component-level. > Link to
Escher C Verifier enables the development of formally-verifiable software in a subset of C (based on MISRA-C 2004). It performs static analysis on the code, checks conformance with many of the MISRA rules, and verifies mathematically that the software is free from run-time errors and "undefined behaviour" for all inputs.
Optionally, Escher C Verifier can also verify that the software meets functional specifications. > Link to
Escher Technologies can provide you with consultancy to assist you with developing your critical software. Our services include DO-178B software development and IEC 61508 software development. > Link to