news
New release of Escher Verification Studio out!
Version 6.10 of EVS is now available. As usual, those of you with a maintenance contract need take no further action,
but if you are using the free edition you will need to contact us to request
a new download key.
A full list of the changes is provided in the readme files accompanying the distribution.
These changes include additional Project Manager features, such
as facilities to help find definitions and occurrences of identifiers.
For users of Perfect Developer, there is a conditional trace
facility.
Users of Escher C Verifier will find support for a wider range of C++
constructs, including class inheritance, protected members, and virtual
functions.
Perfect Developer and BitWise
BitWise Ltd. will use Escher Technologies' flagship
product Perfect Developer to specify and design their most safety-critical systems, for example to IEC61508 SIL4.
More details here
(opens in a separate page)
A major release of Escher Verification Studio
Version 6.0 of EVS has a new built-in editor, with syntax highlighting for both Perfect and C/C++ including the additional eCv keywords.
Diagnostic messages have been improved, with additional information provided for some warning and error types, spanning multiple lines where necessary.
Suggestions for amending the specification to fix verification failures are now included with the verification failure warning message.
When using the new built-in editor, diagnostic messages from Escher Tool can be shown as annotations to the corresponding lines in the source file.
The EVS theorem prover is more powerful and generally faster than before.
eCv now supports a few more constructs from C++. These include extern "C" directives and static member functions of classes and structs. Function overloading is permitted,
with additional constraints to permit safe use of this feature in critical systems.
Now, Perfect Developer supports a 'trace' statement allowing program execution to be traced during development;
and some class member functions can be reimplemented as modifying member schemas, allowing more efficient code to be generated
Fuller details are available in the "readme" files.
If you'd like to use the new version of
Escher Verification Studio,
you'll need a new download key.
news archive
Leave the Archive
Our new tool family described in a book!
(ISBN 13: 9781848213630 ISBN 10: 1848213638; hardback)
A book on the industrial use of formal methods has been published today: it includes a
chapter on the Escher tools, Perfect Developer and eCv. Besides the necessary background
information, there is an example of the use of each tool from a developer's point of view, plus 4 real-world examples
which our clients have kindly allowed us to mention.
More information is available on the publisher's website
here.
(opens in a new window)
Escher and the LOHAN project
LOHAN stands for Low Orbit Helium Assisted Navigator.
We are proud to be official supplier of software verification services to The Register's LOHAN project.
Read all about at it at The Register!
here
(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.
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
(opens in a separate page)
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
(opens in a separate page)
Leave the Archive
|
TOP
