Subject: Re: Accellera: Branching vs. Linear Time
From: Matthew Morley (matthew@verisity.com)
Date: Mon Jul 09 2001 - 21:09:43 PDT
sorry to get into these recent threads rather late... hoped i could
ignore all these emails till the long plane trip to Paris.
... "ed" == Ed Clarke <emc@cs.cmu.edu> writes:
ed> I think the point you make in the second part of your message is
ed> an important one. In addition to deciding on what language to use,
ed> we really need to decide on how compositional reasoning and
ed> refinement should be done as well.
it is an important point, but it occurs to me it might be furitful to
start from a slightly different question: to what degree are these
concerns separable?
we *could* seek a "logical framework" (i use the term tentatively in
the extreme!) for conducting the sort of meta reasoning
M || M' |= p iff M |= f(M') -> p
that is commonly used, such that the proof (p holds) is fully formal.
but wouldn't that be monadic second order logic (making issues of mere
syntax slightly irrelevant)?
that's just one extreme.
at the other end we might conclude something like this: since in any
case in order to do a mechanical proof we'll need deep abstractions in
order to get "M" small & simple enough, and these may be more or less
formally applied, there's little point in a logical framework since
our proofs will be at best "informal." so use any compositional
reasoning methodology you find that works.
straw men, of course.
M
ed> At 11:29 AM 6/25/2001 -0700, Sandeep K. Shukla wrote:
>> An excellent example of an LTL model checker built on top of CTL
>> model checker is Cadence SMV (freely downloadable from Ken
>> Mcmillan's webpage at http://www-cad.eecs.berkeley.edu/~kenmcmil/).
>> In this version of SMV, mostly LTL formulae are used for model
>> checking, but since it is based on CTL at the core, one can
>> actually express CTL properties as well. I routinely used CTL
>> formula to check vacuity in cadence SMV.
>>
>>
>> From my experience with various model checkers, it is the best
>> right now(not necessarily in terms of space and time efficiency,
>> but in terms of the various facilities built into the model
>> checker, for doing induction, symmetry based reduction of data
>> types, assume-guranatee reasoning, data type abstraction etc.) Ken
>> seems to have thought very well what an industrial designer needs
>> in a model checker to facilitate verification. The usage of
>> abstraction layers for assume-guarantee, the facilities to do
>> induction etc impressed me away from using any other model checker.
--
This archive was generated by hypermail 2b28 : Mon Jul 09 2001 - 21:11:18 PDT