Escher Technologies Escher Technologies
Home Tools Services Support News Company Contact Publications Articles
Escher Technologies
arrowEscher Verification Studio
arrowEscher C Verifier
arrowPerfect Developer
arrowEvaluating the tools
arrowWhat others say
arrowCritical embedded software
arrowYour development process
arrowPD and SPARK Ada
arrowSummary of benefits
“We were especially impressed by the automation of verification proofs, which will substantially reduce our costs, and by the level of support provided by Escher Technologies.”

Guy Mason
General Dynamics UK Ltd.

Perfect Developer

Perfect Developer (or PD for short) is a tool for modelling software systems, and providing formal proofs of correctness. Optionally, code can be generated from the model, in a choice of languages.

Perfect Developer:

Perfect Developer - Making software bugs extinct!

Unlike most other formal tools, Perfect Developer delivers high productivity by generating a very high proportion of software verification proofs without user intervention, using state-of-the-art automated reasoning technology.

Don't just take our word for it!

Read what others say about Perfect Developer.

Our tools can help YOU, too.

Here's how it works:

Unlike traditional software development using a standard programming language such as C++ or Java, the Perfect Developer tool allows you to express precisely specifications and user requirements, as well as code, using its specification language, Perfect. A Perfect source file describes not only the data you want to store and the program steps you want to carry out, but also describes

  • what the data represents,
  • the specifications that the program steps are there to satisfy
  • and the requirements that the system or component must meet.

Advanced automated reasoning technology is used to relate the specifications to the requirements, and the program steps to the specifications, generating correctness proofs where possible. Where correctness is in doubt, this is highlighted.

Quite often, you don't need to describe the program steps, since Perfect Developer can generate them automatically. Optionally, Perfect Developer produces an equivalent C++, C# or Java program ready for compilation. SPARK Ada code generation is under development.

For more detail, take a look at this step-by-step guide to software development.


Home    TOPTOP
Copyright © 1997-2017 Escher Technologies Limited. All rights reserved. Information is subject to change without notice.      Link to  Privacy/Cookie Policy (new window)