Subject: RE: Accellera: Branching vs. Linear Time
From: Sandeep K. Shukla (skshukla@ics.uci.edu)
Date: Sun Jul 15 2001 - 00:59:00 PDT
>
> First, I am not peddling anything. Second, while I would not argue for
> inseparability, a complete separation is not defensible, IMHO. The
> purpose of the language is to be used, so the language has to support
> reasonable modes of usage. For example, Verisity contemplates people
> using Temporal e for both simulation and model checking, so you have put
> some effort to accomplish this integration (as we have done in ForSpec).
> Similarly, the ForSpec team believes that compositoinal verification is
> importat, so ForSpec offers full supports for that. We are not proposing
> compositional verification any more than you are proposing simulation.
> We both present features of the languages. It is up to the members
> of the Commttee to decide how important these features are.
I think language should be developed hand in hand with methodology.
Again drawing from Cadence SMV experience, since the methodology
in SMV supports symmetry based reduction, induction, etc as a part
of methodology, it has as part of the language ordset, symmetry set etc,
as well as for supporting the refinement mapping based methodology,
it has as part of language "using prove" , "layer" etc.
>
> From what I have in a public talk, Intel reported on a large verification
> team without a single PhD holder.
The manager of that team did not like to hire PhDs for a long time, but
later
hired a few, and also mostly the team was helped by well known FV people
like
Carl Seger, Robert Jones, Mark Aaagard etc who are not only PhDs but are
experts in theorem proving etc.
> > Cadence SMV is an excellent FV tool. Its property language is LTL with
> free variables. It was one of the starting point for the deveopment of
> ForSpec.
>
Does any one know of a model checker which also has first order arithmetic
built into
it and does not include arithmetic as a part of the state? ALso does any one
know of
a model checker for probabilistic transition system and probabilistic
assertions? I am
looking for one at this moment and will be grateful if some one can point me
out to one?
regards
Sandeep
>
This archive was generated by hypermail 2b28 : Wed Jul 11 2001 - 01:04:46 PDT