news
David's blog
(opens in a new window)
Escher Verification Studio
Our NEW tool, Escher C Verifier (eCv), has been released, as part of Escher Verification Studio.
eCv provides formal verification of MISRA-C code by applying
the principles of Verified Design by Contract. Escher C Verifier and
Perfect Developer (PD) use the same theorem prover.
We anticipated that certain customers would wish to use PD for specification,
directly followed by eCv. We have therefore combined both tools
into a single product - Escher Verification Studio - with PD
and eCv as components of this product. Commercial users
may buy a licence for just one component or for both of them.
As newsletter-subscribers will already be aware, existing PD users will find
that the names of some files and the
installation directory structure have changed, because of this repackaging.
More information is available
here
(PDF; opens in a new window)
The Educational Edition of PD 4.10
continues to be available for download from us.
If you're currently using a pre-2010 version of PD Free Edition, and you'd like to use
either Escher Verification Studio or the earlier stand-alone PD 4.10,
you'll need a new download key.
Phaedrus Systems appointed as UK distributor
With the launch of our new tool family, we are delighted to announce the appointment of
Phaedrus Systems as UK distributor for Escher Technologies. Phaedrus Systems is
the leading supplier of tools and services to the developers of embedded safety-critical
and high-integrity systems.
More information is available on their website
here
(opens in a new window)
Perfect Developer New Release: Version 4.10
The Free Edition of PD 4.10 is now available.
If you're currently using an earlier version of PD Free Edition, and you'd like to use the new version,
you'll need a new download key.
The Critical Systems Edition of PD 4.10 is now available as a
Release Candidate.
As requested by our commercial customers,
Perfect now supports:
- class history invariants, with the option to exempt
certain schemas from having to obey them
-
properties with postconditions, which
provides a convenient way of describing expected consequences
of calling schemas, especially where multiple variables are modified.
Also, we now provide partial support for
code generation in smaller subsets of C++ ("Embedded C++") and Ada ("SPARK Ada"),
making it easier
to avoid dynamic memory allocation in the generated code.
Plus many smaller improvements and fixes which are detailed in the readme
file accompanying the download.
David's New Verification Blog
Today, David started a Verification Blog. (opens in a new window)
David intends to focus on
the use of C and C++ in critical systems - in particular, on language subsets
such as MISRA-C, MISRA-C++ and JSF C++, and on formal verification
tools for C and C++, such as the forthcoming eCv
tool (formerly called ArC)
from Escher Technologies.
Perfect Developer and GDUK
General Dynamics UK Ltd. will use Escher Technologies’ flagship product Perfect Developer
to specify and design a safety-critical airborne stores management system.
More details here
Perfect Developer Version 4 released
PD 4.0 brings improvements to many areas of the product, including:
- The Perfect language has been extended to support exceptions
- In addition to C++ and Java, the code generators can now generate C# 2.0 code,
and we provide a C# version of the Perfect runtime library
- C++ code generation has been reworked to
support 16-bit character sets and to resolve incompatibilities
with strictly-conforming compilers such as gcc 4.3
- Several improvements have been made to the theorem prover
More details can be found in the Perfect Developer 4.0
readme file (available in the download package).
Our paper on mathematical verification of C programs
was presented at SEFM in September 2007.
If you missed it, read the paper here...
Perfect Developer and Grand Challenge 6
We're proud to announce the involvement of Escher Technologies with this challenge.
Full article here
|
TOP
