two 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 in
Escher Verification Studio.
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.
Perfect Developer
is 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.
|