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

–吃

PAM: A process algebra manipulator, by directly manipulating process terms. The logic that PAM implements is equational logic plus recursion, with some features tailored to the particular requirements of process algebras. Equational reasoning is implemented by rewriting, while recursion is dealt with by induction. Proofs are construc

incite

A proof assistant for PSF, on state space exploration, we use an axiomatic approach. The axioms we use for the construction of proofs, are based on ACP. Besides these standard axioms we also consider tactics for shortening proofs. We use PSF (Process Specification Formalism), an extension of ACP with abstract data types, to

Inclement

Guileless

Lecture Notes in Computer Sciencehttp://image.papertrans.cn/c/image/233351.jpg

hair-bulb

Computer Aided Verification978-3-540-46763-2Series ISSN 0302-9743 Series E-ISSN 1611-3349

left-ventricle

Denis Cavallucci,Stelian Brad,Pavel Livotovyer-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.

柔美流畅

caldron

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.

Expostulate

Avoiding state explosion by composition of minimal covering graphs,cation of Petri nets properties from the point of view of reusability of partial results already obtained. We give two algorithms which allow to compute the minimal covering graph of a Petri net by composing the minimal covering graphs of each of its modules.

故意钓到白杨

Procure Software Delivery EnvironmentWe present a sound and complete tableau proof system for establishing whether a set of elements of an arbitrary transition system model has a property expressed in (a slight extension of) the modal mu-calculus. The proof system, we beleive, offers a very general verification method applicable to a wide range of computational systems.