Übersicht			Auf mobile öffnen

Lieferstatus:	Auf Bestellung (Lieferzeit unbekannt)
Veröffentlichung:	Juni 2003
Genre:	EDV / Informatik
	C / Computer architecture & logic design / Computer logic / Computer programming / software engineering / computer science / Computer Science Logic and Foundations of Programming / Computers / Expert systems / knowledge-based systems / Formal Languages and Automata Theory / Logic Design / Logics and Meanings of Programs / Mathematical logic / Mathematical Logic and Formal Languages / Mathematical theory of computation / Rechnerarchitektur und Logik-Entwurf / Software Engineering / Special Purpose and Application-Based Systems / Special purpose computers / Theory of Computation / Wissensbasierte Systeme, Expertensysteme mehr...
ISBN:	9783540405245
EAN-Code:	9783540405245
Verlag:	Springer EN
Einband:	Kartoniert
Sprache:	English
Serie:	#2725 - Lecture Notes in Computer Science
Dimensionen:	H 233 mm / B 155 mm / D
Gewicht:	1470 gr
Seiten:	462
Illustration:	XII, 462 p.
Zus. Info:	EUDR exemption - product or manufacturing materials placed on the market prior to 31.12.2025.
Bewertung:	Titel bewerten / Meinung schreiben

Inhalt:

Extending Bounded Model Checking.- Interpolation and SAT-Based Model Checking.- Bounded Model Checking and Induction: From Refutation to Verification.- Symbolic Model Checking.- Reasoning with Temporal Logic on Truncated Paths.- Structural Symbolic CTL Model Checking of Asynchronous Systems.- A Work-Efficient Distributed Algorithm for Reachability Analysis.- Games, Trees, and Counters.- Modular Strategies for Infinite Games on Recursive Graphs.- Fast Mu-Calculus Model Checking when Tree-Width Is Bounded.- Dense Counter Machines and Verification Problems.- Tool Presentations I.- TRIM: A Tool for Triggered Message Sequence Charts.- Model Checking Multi-Agent Programs with CASP.- Monitoring Temporal Rules Combined with Time Series.- FAST: Fast Acceleration of Symbolic Transition Systems.- Rabbit: A Tool for BDD-Based Verification of Real-Time Systems.- Abstraction I.- Making Predicate Abstraction Efficient:.- A Symbolic Approach to Predicate Abstraction.- Unbounded, Fully Symbolic Model Checking of Timed Automata Using Boolean Methods.- Dense Time.- Digitizing Interval Duration Logic.- Timed Control with Partial Observability.- Hybrid Acceleration Using Real Vector Automata.- Tool Presentations II.- Abstraction and BDDs Complement SAT-Based BMC in DiVer.- TLQSolver: A Temporal Logic Query Checker.- Evidence Explorer: A Tool for Exploring Model-Checking Proofs.- HERMES: An Automatic Tool for Verification of Secrecy in Security Protocols.- Infinite State Systems.- Iterating Transducers in the Large.- Algorithmic Improvements in Regular Model Checking.- Efficient Image Computation in Infinite State Model Checking.- Abstraction II.- Thread-Modular Abstraction Refinement.- A Game-Based Framework for CTL Counterexamples and 3-Valued Abstraction-Refinement.- Abstraction for Branching Time Properties.- Applications.- Certifying Optimality of State Estimation Programs.- Domain-Specific Optimization in Automata Learning.- Model Checking Conformance with Scenario-Based Specifications.- Theorem Proving.- Deductive Verification of Advanced Out-of-Order Microprocessors.- Theorem Proving Using Lazy Proof Explication.- Automata-Based Verification.- Enhanced Vacuity Detection in Linear Temporal Logic.- Bridging the Gap between Fair Simulation and Trace Inclusion.- An Improved On-the-Fly Tableau Construction for a Real-Time Temporal Logic.- Invariants.- Strengthening Invariants by Symbolic Consistency Testing.- Linear Invariant Generation Using Non-linear Constraint Solving.- Explicit Model Checking.- To Store or Not to Store.- Calculating ?-Confluence Compositionally.