RE: [sc] compiler and scripting language validation

RE: [sc] compiler and scripting language validation

From: Rod Chapman ^lt;rod.chapman@xxxxxx>
Date: Thu 13 Apr 2006 - 14:10:26 BST
Message-ID: <FE9BBC7565566346B5BB591F924FA1890172066F@xxxxxx>
>  * SCADE includes technology for proof of assertions. The 
> assertions are directly derived from the requirements. From 
> my understanding, this is a more powerful assertion prover 
> than the SPARC equivalent. (I will be interested in any 
> specific contradiction or support for this opinion).

This is news to us...Are you referring to the
SCADE "Design Verifier" product?  Esterel's
web-site here:

makes many claims, and includes a note in small print:

"SCADE Design Verifier is based on the Prover Plug-In. Prover Plug-In is
a trademark of Prover Techbology AB..."

I am not familiar with this technology.  Can anyone shed any light
on its expressive power, decideability etc etc?

 - Rod's SPARK not SPARC (the latter is a vigorously defended trademark... :-) )


This email is confidential and intended solely for the use of the individual to whom it is addressed.  If you are not the intended recipient, be advised that you have received this email in error and that any use, disclosure, copying or distribution or any action taken or omitted to be taken in reliance on it is strictly prohibited.  If you have received this email in error please contact the sender.  Any views or opinions presented in this email are solely those of the author and do not necessarily represent those of Praxis High Integrity Systems Ltd (Praxis HIS). 

 Although this email and any attachments are believed to be free of any virus or other defect, no responsibility is accepted by Praxis HIS or any of its associated companies for any loss or damage arising in any way from the receipt or use thereof.  The IT Department at Praxis HIS can be contacted at

Received on Thu Apr 13 14:10:29 2006