Computer Aided Verification 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings /

• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Άλλοι συγγραφείς: Hunt, Jr., Warren A. (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt), Somenzi, Fabio (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2003.
• Έκδοση: 1st ed. 2003.
• Σειρά: Lecture Notes in Computer Science, 2725
• Θέματα: Computers.; Computer logic.; Logic design.; Special purpose computers.; Software engineering.; Mathematical logic.; Theory of Computation.; Logics and Meanings of Programs.; Logic Design.; Special Purpose and Application-Based Systems.; Software Engineering.; Mathematical Logic and Formal Languages.

Πίνακας περιεχομένων:

• 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.