How temporal-e supports the assume/guarantee paradigm


Subject: How temporal-e supports the assume/guarantee paradigm
From: Armoni, Roy (roy.armoni@intel.com)
Date: Mon Jul 16 2001 - 12:38:15 PDT


I would like to add to Moshe's request that it would be nice if someone
from Verisity could answer this question with respect to soundness,
completeness and tractability.

To be fair, I would like to note that a thread on this issue has already
been started with IBM on Sugar.

Regards, Roy

-----Original Message-----
From: vardi@cs.rice.edu [mailto:vardi@cs.rice.edu]
Sent: Thursday, July 12, 2001 6:14 PM
To: eisner@il.ibm.com; roy.armoni@intel.com
Cc: vfv@eda.org
Subject: Re: FTL fully supports that assume/guarantee paradigm

We went to a great length to describe rigorously what we mean by
fully supporting the assume/guarantee paradigm. It is now time
to hear from both IBM and Verisity, who also claim support of the
paradigm in their language, what exactly they support and what is the
precise meaning of assume-guarantee in their language.

Moshe



This archive was generated by hypermail 2b28 : Mon Jul 16 2001 - 12:38:56 PDT