Willkommen, schön sind Sie da!
Logo Ex Libris

Computer Aided Verification

  • Kartonierter Einband
  • 462 Seiten
(0) Erste Bewertung abgeben
Alle Bewertungen ansehen
The refereed proceedings of the 15th International Conference on Computer Aided Verification, CAV 2003, held in Boulder, CO, USA i... Weiterlesen
135.00 CHF 108.00
Sie sparen CHF 27.00
Exemplar wird für Sie besorgt.
Kein Rückgaberecht!
Bestellung & Lieferung in eine Filiale möglich


The refereed proceedings of the 15th International Conference on Computer Aided Verification, CAV 2003, held in Boulder, CO, USA in July 2003.

The 32 revised full papers and 9 tool papers presented were carefully reviewed and selected from a total of 102 submissions. The papers are organized in topical sections on bounded model checking; symbolic model checking; games, trees, and counters; tools; abstraction; dense time; infinite state systems; applications; theorem proving; automata-based verification; invariants; and explicit model checking.

Includes supplementary material: sn.pub/extras

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.


Titel: Computer Aided Verification
Untertitel: 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings
EAN: 9783540405245
ISBN: 978-3-540-40524-5
Format: Kartonierter Einband
Herausgeber: Springer, Berlin
Genre: Informatik
Anzahl Seiten: 462
Gewicht: 667g
Größe: H235mm x B235mm x T155mm
Jahr: 2003
Untertitel: Englisch
Auflage: 2003

Weitere Produkte aus der Reihe "Lecture Notes in Computer Science"