Computer Aided Verification 3rd International Workshop, CAV '91, Aalborg, Denmark, July 1-4, 1991. Proceedings / edited by Kim G. Larsen, Arne Skou.

This volume contains the proceedings of the third International Workshop on Computer Aided Verification, CAV '91, held in Aalborg, Denmark, July 1-4, 1991. The objective of this series of workshops is to bring together researchers and practitioners interested in the development and use of metho...

Full description

Saved in:
Bibliographic Details
Corporate Author: SpringerLink (Online service)
Other Authors: Larsen, Kim G. (Editor), Skou, Arne (Editor)
Format: eBook
Language:English
Published: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 1992.
Edition:1st ed. 1992.
Series:Lecture Notes in Computer Science, 575
Springer eBook Collection.
Subjects:
Online Access:Click to view e-book
Holy Cross Note:Loaded electronically.
Electronic access restricted to members of the Holy Cross Community.

MARC

LEADER 00000nam a22000005i 4500
001 b3241426
003 MWH
005 20191028122009.0
007 cr nn 008mamaa
008 121227s1992 gw | s |||| 0|eng d
020 |a 9783540467632 
024 7 |a 10.1007/3-540-55179-4  |2 doi 
035 |a (DE-He213)978-3-540-46763-2 
050 4 |a E-Book 
072 7 |a UY  |2 bicssc 
072 7 |a COM014000  |2 bisacsh 
072 7 |a UY  |2 thema 
072 7 |a UYA  |2 thema 
245 1 0 |a Computer Aided Verification  |h [electronic resource] :  |b 3rd International Workshop, CAV '91, Aalborg, Denmark, July 1-4, 1991. Proceedings /  |c edited by Kim G. Larsen, Arne Skou. 
250 |a 1st ed. 1992. 
264 1 |a Berlin, Heidelberg :  |b Springer Berlin Heidelberg :  |b Imprint: Springer,  |c 1992. 
300 |a XI, 493 p.  |b online resource. 
336 |a text  |b txt  |2 rdacontent 
337 |a computer  |b c  |2 rdamedia 
338 |a online resource  |b cr  |2 rdacarrier 
347 |a text file  |b PDF  |2 rda 
490 1 |a Lecture Notes in Computer Science,  |x 0302-9743 ;  |v 575 
490 1 |a Springer eBook Collection 
505 0 |a Taming infinite state spaces -- Silence is golden: Branching bisimilarity is decidable for context-free processes -- Computing distinguishing formulas for branching bisimulation -- Compositional checking of satisfaction -- An action based framework for verifying logical and behavioural properties of concurrent systems -- A linear-time model-checking algorithm for the alternation-free modal mu-calculus -- Automatic temporal verification of buffer systems -- Mechanically checked proofs of kernel specifications -- A top down approach to the formal specification of SCI cache coherence -- Integer programming in the analysis of concurrent systems -- The lotos model of a fault protected system and its verification using a petri net based approach -- Error diagnosis in finite communicating systems -- Temporal precondition verification of design transformations -- PAM: A process algebra manipulator -- The Concurrency Workbench with priorities -- A proof assistant for PSF -- Avoiding state explosion by composition of minimal covering graphs -- “On the fly” verification of behavioural equivalences and preorders -- Bounded-memory algorithms for verification on-the-fly -- Generating BDDs for symbolic model checking in CCS -- Vectorized symbolic model checking of computation tree logic for sequential machine verification -- Functional extension of symbolic model checking -- An automated proof technique for finite-state machine equivalence -- From data structure to process structure -- Checking for language inclusion using simulation preorders -- A semantic driven method to check the fineteness of CCS processes -- Using the HOL prove assistant for proving the correctness of term rewriting rules reducing terms of sequential behavior -- Mechanizing a proof by induction of process algebra specifications in higher order logic -- A two-level formal verification methodology using HOL and COSMOS -- Efficient algorithms for verification of equivalences for probabilistic processes -- Partial-order model checking: A guide for the perplexed -- Using partial orders for the efficient verification of deadlock freedom and safety properties -- Complexity results for POMSET languages -- Mechanically verifying safety and liveness properties of delay insensitive circuits -- Automating most parts of hardware proofs in HOL -- An overview and synthesis on timed process algebras -- Minimum and maximum delay problems in realtime systems -- Formal verification of speed-dependent asynchronous circuits using symbolic model checking of Branching Time Regular Temporal Logic -- Verifying properties of HMS machine specifications of real-time systems -- A linear time process algebra -- Deciding properties of regular real timed processes -- An algebra of Boolean processes -- Comparing generic state machines -- An automata theoretic approach to Temporal Logic. 
520 |a This volume contains the proceedings of the third International Workshop on Computer Aided Verification, CAV '91, held in Aalborg, Denmark, July 1-4, 1991. The objective of this series of workshops is to bring together researchers and practitioners interested in the development and use of methods, tools and theories for automatic verification of (finite) state systems. The workshop provides a unique opportunity for comparing the numerous verification methods and associated verification tools, and the extent to which they may be utilized in application design. The emphasis is not only on new research results but also on the application of existing results to real verification problems. The papers in the volume areorganized into sections on equivalence checking, model checking, applications, tools for process algebras, the state explosion problem, symbolic model checking, verification and transformation techniques, higher order logic, partial order approaches, hardware verification, timed specification and verification, and automata. 
590 |a Loaded electronically. 
590 |a Electronic access restricted to members of the Holy Cross Community. 
650 0 |a Computers. 
650 0 |a Software engineering. 
650 0 |a Architecture, Computer. 
650 0 |a Computer logic. 
650 0 |a Mathematical logic. 
650 0 |a Special purpose computers. 
690 |a Electronic resources (E-books) 
700 1 |a Larsen, Kim G.  |e editor.  |4 edt  |4 http://id.loc.gov/vocabulary/relators/edt 
700 1 |a Skou, Arne.  |e editor.  |4 edt  |4 http://id.loc.gov/vocabulary/relators/edt 
710 2 |a SpringerLink (Online service) 
773 0 |t Springer eBooks 
830 0 |a Lecture Notes in Computer Science,  |x 0302-9743 ;  |v 575 
830 0 |a Springer eBook Collection. 
856 4 0 |u https://holycross.idm.oclc.org/login?auth=cas&url=https://doi.org/10.1007/3-540-55179-4  |3 Click to view e-book  |t 0 
907 |a .b32414262  |b 04-18-22  |c 02-26-20 
998 |a he  |b 02-26-20  |c m  |d @   |e -  |f eng  |g gw   |h 0  |i 1 
912 |a ZDB-2-SCS 
912 |a ZDB-2-LNC 
912 |a ZDB-2-BAE 
950 |a Computer Science (Springer-11645) 
902 |a springer purchased ebooks 
903 |a SEB-COLL 
945 |f  - -   |g 1  |h 0  |j  - -   |k  - -   |l he   |o -  |p $0.00  |q -  |r -  |s b   |t 38  |u 0  |v 0  |w 0  |x 0  |y .i21545911  |z 02-26-20 
999 f f |i f4428035-1173-5fee-b95a-4a5c5979b0bb  |s af605091-e18d-5aa9-9c1e-543a5c709891  |t 0 
952 f f |p Online  |a College of the Holy Cross  |b Main Campus  |c E-Resources  |d Online  |t 0  |e E-Book  |h Library of Congress classification  |i Elec File