Keywords:
Computer Communication Networks
;
Logic design
;
Logic, Symbolic and mathematical
;
Computer science
;
Software engineering
;
Machine theory.
;
Mathematical logic.
;
Computers, Special purpose.
;
Computer Communication Networks
;
Mathematical Logic and Formal Languages
;
Computer Science
;
Mathematical Logic and Foundations
;
Logics and Meanings of Programs
;
Special Purpose and Application-Based Systems
;
Software Engineering
;
Konferenzschrift N.J., 1990
;
Verifikation
Description / Table of Contents:
Temporal logic model checking: Two techniques for avoiding the state explosion problem -- Automatic verification of extensions of hardware descriptions -- Papetri : Environment for the analysis of PETRI nets -- Verifying temporal properties of sequential machines without building their state diagrams -- Formal verification of digital circuits using symbolic ternary system models -- Vectorized model checking for computation tree logic -- to a computational theory and implementation of sequential hardware equivalence -- Auto/autograph -- A data path verifier for register transfer level using temporal logic language Tokio -- The use of model checking in ATPG for sequential circuits -- Compositional design and verification of communication protocols, using labelled petri nets -- Issues arising in the analysis of L.0 -- Automated RTL verification based on predicate calculus -- On using protean to verify ISO FTAM protocol -- Quantitative temporal reasoning -- Using partial-order semantics to avoid the state explosion problem in asynchronous systems -- A stubborn attack on state explosion -- Using optimal simulations to reduce reachability graphs -- Using partial orders to improve automatic verification methods -- Compositional minimization of finite state systems -- Minimal model generation -- A context dependent equivalence relation between kripke structures -- The modular framework of computer-aided verification -- Verifying liveness properties by verifying safety properties -- Memory efficient algorithms for the verification of temporal properties -- A unified approach to the deadlock detection problem in networks of communicating finite state machines -- Branching time regular temporal logic for model checking with linear time complexity -- The algebraic feedback product of automata -- Synthesizing processes and schedulers from temporal specifications -- Task-driven supervisory control of discrete event systems -- A proof lattice-based technique for analyzing liveness of resource controllers -- Verification of a multiprocessor cache protocol using simulation relations and higher-order logic (summary) -- Computer assistance for program refinement -- Program verification by symbolic execution of hyperfinite ideal machines -- Extension of the Karp and miller procedure to lotos specifications -- An algebra for delay-insensitive circuits -- Finiteness conditions and structural construction of automata for all process algebras -- On automatically explaining bisimulation inequivalence.
Type of Medium:
Online Resource
Pages:
Online-Ressource (XIII, 372 S.)
Edition:
Online-Ausg. Berlin [u.a.] Springer 2006 Springer lecture notes archive
ISBN:
9783540383949
Series Statement:
Lecture notes in computer science 531
URL:
http://www.springerlink.com/content/n73145341v27
URL:
http://www.springerlink.de/openurl.asp?genre=book&isbn=978-3-540-54477-7
URL:
http://dx.doi.org/10.1007/BFb0023712
URL:
https://doi.org/10.1007/BFb0023712
URL:
https://zbmath.org/?q=an:0756.00006
Language:
English
Note:
Literaturangaben
Permalink
