Escher Technologies - Tools (original) (raw)
three tools to reduce the cost of your critical software development
Perfect Developer is designed for use during specification and software design, while Escher C Verifier is designed for use during coding when the language is C. Both Escher C Verifier and Perfect Developer are included inEscher Verification Studio. They can be licensed together or separately, as required.
Similarly, Escher C++ Verifier is designed for use during coding when the language is C++.
Escher C Verifier enables the development of formally-verifiable software in a subset of C (based on MISRA-C 2012). 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.
Perfect Developeris a tool for specifying and modelling 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.