Computer-Aided Verification
Springer Berlin (Verlag)
978-3-540-54477-7 (ISBN)
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.
Erscheint lt. Verlag | 2.10.1991 |
---|---|
Reihe/Serie | Lecture Notes in Computer Science |
Zusatzinfo | XIV, 378 p. |
Verlagsort | Berlin |
Sprache | englisch |
Maße | 155 x 235 mm |
Gewicht | 641 g |
Themenwelt | Mathematik / Informatik ► Informatik |
Mathematik / Informatik ► Mathematik ► Allgemeines / Lexika | |
Schlagworte | algorithm • algorithms • Attribut • Computer • Computer-Aided Verification • Computerunterstütztes Verfahren • Computer-unterstützte Verifikation • Formale Sprache • formale Sprachen • formal language • Formal Languages • Formal Verification • Hardcover, Softcover / Informatik, EDV/Informatik • HC/Informatik, EDV/Informatik • Network Protocols • Netzwerkprotokolle • Reasoning about Programs • Semantics of Programming Languages • Semantik von Programmiersprachen • session • Software Engineering / Softwareentwicklung • Softwareentwicklung • Tools • verification • Verifikation (EDV) |
ISBN-10 | 3-540-54477-1 / 3540544771 |
ISBN-13 | 978-3-540-54477-7 / 9783540544777 |
Zustand | Neuware |
Haben Sie eine Frage zum Produkt? |
aus dem Bereich