Übersicht			Auf mobile öffnen

Lieferstatus:	Auf Bestellung (Lieferzeit unbekannt)
Veröffentlichung:	Juli 2001
Genre:	EDV / Informatik
	Artificial Intelligence / C / Computer architecture & logic design / Computer logic / Computer programming / software engineering / computer science / Computer Science Logic and Foundations of Programming / Computers / Database Management / database programming / Formal Languages and Automata Theory / Logics and Meanings of Programs / Mathematical logic / Mathematical Logic and Formal Languages / Mathematical theory of computation / Operating systems / Software Engineering / Software Engineering/Programming and Operating Systems / Theory of Computation mehr...
ISBN:	9783540423454
EAN-Code:	9783540423454
Verlag:	Springer EN
Einband:	Kartoniert
Sprache:	English
Serie:	#2102 - Lecture Notes in Computer Science
Dimensionen:	H 233 mm / B 155 mm / D
Gewicht:	1650 gr
Seiten:	522
Illustration:	XIII, 522 p.
Zus. Info:	EUDR exemption - product or manufacturing materials placed on the market prior to 31.12.2025.
Bewertung:	Titel bewerten / Meinung schreiben

Inhalt:

Invited Talk.- Software Documentation and the Verification Process.- Model Checking and Theorem Proving.- Certifying Model Checkers.- Formalizing a JVML Verifier for Initialization in a Theorem Prover.- Automated Inductive Verification of Parameterized Protocols?.- Automata Techniques.- Efficient Model Checking Via Büchi Tableau Automata?.- Fast LTL to Büchi Automata Translation.- A Practical Approach to Coverage in Model Checking.- Verification Core Technology.- A Fast Bisimulation Algorithm.- Symmetry and Reduced Symmetry in Model Checking?.- Transformation-Based Verification Using Generalized Retiming.- BDD and Decision Procedures.- Meta-BDDs: A Decomposed Representation for Layered Symbolic Manipulation of Boolean Functions.- CLEVER: Divide and Conquer Combinational Logic Equivalence VERification with False Negative Elimination.- Finite Instantiations in Equivalence Logic with Uninterpreted Functions.- Abstraction and Refinement.- Model Checking with Formula-Dependent Abstract Models.- Verifying Network Protocol Implementations by Symbolic Refinement Checking.- Automatic Abstraction for Verification of Timed Circuits and Systems?.- Combinations.- Automated Verification of a Randomized Distributed Consensus Protocol Using Cadence SMV and PRISM?.- Analysis of Recursive State Machines.- Parameterized Verification with Automatically Computed Inductive Assertions?.- Tool Presentations: Rewriting and Theorem-Proving Techniques.- EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality, and Conservative Transformations.- AGVI - Automatic Generation, Verification, and Implementation of Security Protocols.- ICS: Integrated Canonizer and Solver?.- µCRL: A Toolset for Analysing Algebraic Specifications.- Truth/SLC - A Parallel Verification Platform for Concurrent Systems.- The SLAM Toolkit.- Invited Talk.- Java Bytecode Verification: An Overview.- Infinite State Systems.- Iterating Transducers.- Attacking Symbolic State Explosion.- A Unifying Model Checking Approach for Safety Properties of Parameterized Systems.- A BDD-Based Model Checker for Recursive Programs.- Temporal Logics and Verification.- Model Checking the World Wide Web?.- Distributed Symbolic Model Checking for ?-Calculus.- Tool Presentations: Model-Checking and Automata Techniques.- The Temporal Logic Sugar.- TReX: A Tool for Reachability Analysis of Complex Systems.- BOOSTER: Speeding Up RTL Property Checking of Digital Designs by Word-Level Abstraction.- SDLcheck: A Model Checking Tool.- EASN: Integrating ASN.1 and Model Checking.- Rtdt: A Front-End for Efficient Model Checking of Synchronous Timing Diagrams.- TAXYS: A Tool for the Development and Verification of Real-Time Embedded Systems?.- Microprocessor Verification, Cache Coherence.- Microarchitecture Verification by Compositional Model Checking.- Rewriting for Symbolic Execution of State Machine Models.- Using Timestamping and History Variables to Verify Sequential Consistency.- SAT, BDDs, and Applications.- Benefits of Bounded Model Checking at an Industrial Setting.- Finding Bugs in an Alpha Microprocessor Using Satisfiability Solvers.- Towards Efficient Verification of Arithmetic Algorithms over Galois Fields GF(2m).- Timed Automata.- Job-Shop Scheduling Using Timed Automata?.- As Cheap as Possible: Effcient Cost-Optimal Reachability for Priced Timed Automata.- Binary Reachability Analysis of Pushdown Timed Automata with Dense Clocks.