Computer aided verification : 3rd international workshop, CAV '91, Aalborg, Denmark, July 1-4, 1991 : proceedings
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...
Na minha lista:
| Autor Corporativo: | |
|---|---|
| Outros Autores: | , |
| Formato: | Livre numérique |
| Idioma: | Anglais |
| Publicado em: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| Colecção: | Lecture notes in computer science
575 |
| Assuntos: | |
| Acesso em linha: | Accès sur la plateforme de l'éditeur Accès sur la plateforme Istex Accès Université d'Orléans Accès INSA CVL |
| Nota: |
Archives Springer e-books (Licence nationale) Archives Springer e-books (Licence nationale) |
| Autres localisations: | Voir dans le Sudoc |
| Edition sous un autre format: | • Computer aided verification, 3rd international workshop, CAV '91, Aalborg, Denmark, July 1-4, 1991, proceedings, K.G. Larsen, A. Skou (eds.), Berlin, Springer-Verlag, 1992, 1 vol. (X-487 p.), Lecture notes in computer science, 3-540-55179-4 • Computer Aided Verification, Texte imprimé, 9783662167816 |
Sumário:
- 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.