Titlebook: Computer Aided Verification; 3rd International Wo Kim G. Larsen,Arne Skou Conference proceedings 1992 Springer-Verlag Berlin Heidelberg 199

Braggart

书目名称Computer Aided Verification影响因子(影响力)




书目名称Computer Aided Verification影响因子(影响力)学科排名




书目名称Computer Aided Verification网络公开度




书目名称Computer Aided Verification网络公开度学科排名




书目名称Computer Aided Verification被引频次




书目名称Computer Aided Verification被引频次学科排名




书目名称Computer Aided Verification年度引用




书目名称Computer Aided Verification年度引用学科排名




书目名称Computer Aided Verification读者反馈




书目名称Computer Aided Verification读者反馈学科排名

防锈

Habituate

An action based framework for verifying logical and behavioural properties of concurrent systems,s algebra and its associated logics. The logic is an action based version of the branching time logic CTL which we call ACTL; it is interpreted over transition labelled structures while CTL is interpreted over state labelled ones. The core of the system are two existing tools, AUTO and EMC. The firs

pus840

A linear-time model-checking algorithm for the alternation-free modal mu-calculus,ystems of equations. This logic is as expressive as the alternation-free fragment of the modal mu-calculus identified by Emerson and Lei, and it may therefore be used to encode a number of temporal logics and behavioral preorders. Our algorithm determines whether a process satisfies a formula in tim

HAIL

Automatic temporal verification of buffer systems,em for verifying RTL definable properties of such systems. The proof method is modular. Although our method is not complete, we feel, as illustrated by the example, that it can be applied to some practical examples. Theorem 3.1 holds for any fragment . of temporal logic as long as the formulae in .

啜泣

Mechanically checked proofs of kernel specifications,yer-Moore theorem prover to prove the correctness of an implementation. The kernel specification had first been given in terms of a labeled transition system. It was transcribed into the Boyer-Moore logic so that an attempt could be made to mechanically check correctness proofs.

啜泣

A top down approach to the formal specification of SCI cache coherence,andard called the Scalable Coherent Interface. We first give the the most abstract (top level) specification of a memory system. We then introduce a private cache for each processor, and specify the notion of cache coherence. We refine the specifications of the memory operations for use with caches,

monogamy

The lotos model of a fault protected system and its verification using a petri net based approach,st. Contrary to other similar Petri net based techniques, our approach avoids to build the whole Petri net from the Lotos specification before verification. In contrast to finite automata based methods, our method can analyse Lotos systems with unbounded state spaces. Our method is founded on a Plac

vasospasm

analogous