Computer Aided Verification 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005. Proceedings /

• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Άλλοι συγγραφείς: Etessami, Kousha (Επιμελητής έκδοσης), Rajamani, Sriram K. (Επιμελητής έκδοσης)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg, 2005.
• Σειρά: Lecture Notes in Computer Science, 3576
• Θέματα: Computer science.; Logic design.; Software engineering.; Computer logic.; Mathematical logic.; Artificial intelligence.; Computer Science.; Logics and Meanings of Programs.; Software Engineering.; Mathematical Logic and Formal Languages.; Artificial Intelligence (incl. Robotics).; Logic Design.

This volume contains the proceedings of the International Conference on Computer Aided Veri?cation (CAV), held in Edinburgh, Scotland, July 6–10, 2005. CAV 2005 was the seventeenth in a series of conferences dedicated to the advancement of the theory and practice of computer-assisted formal an- ysis...

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

• Invited Talks
• Randomized Algorithms for Program Analysis and Verification
• Validating a Modern Microprocessor
• Algorithmic Algebraic Model Checking I: Challenges from Systems Biology
• Tools Competition
• SMT-COMP: Satisfiability Modulo Theories Competition
• Abstraction and Refinement
• Predicate Abstraction via Symbolic Decision Procedures
• Interpolant-Based Transition Relation Approximation
• Concrete Model Checking with Abstract Matching and Refinement
• Abstraction for Falsification
• Bounded Model Checking
• Bounded Model Checking of Concurrent Programs
• Incremental and Complete Bounded Model Checking for Full PLTL
• Abstraction Refinement for Bounded Model Checking
• Symmetry Reduction in SAT-Based Model Checking
• Tool Papers I
• Saturn: A SAT-Based Tool for Bug Detection
• JVer: A Java Verifier
• Building Your Own Software Model Checker Using the Bogor Extensible Model Checking Framework
• Wolf – Bug Hunter for Concurrent Software Using Formal Methods
• Model Checking x86 Executables with CodeSurfer/x86 and WPDS++
• The ComFoRT Reasoning Framework
• Verification of Hardware, Microcode, and Synchronous Systems
• Formal Verification of Pentium ® 4 Components with Symbolic Simulation and Inductive Invariants
• Formal Verification of Backward Compatibility of Microcode
• Compositional Analysis of Floating-Point Linear Numerical Filters
• Syntax-Driven Reachable State Space Construction of Synchronous Reactive Programs
• Games and Probabilistic Verification
• Program Repair as a Game
• Improved Probabilistic Models for 802.11 Protocol Verification
• Probabilistic Verification for “Black-Box” Systems
• On Statistical Model Checking of Stochastic Systems
• Tool Papers II
• The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications
• The Orchids Intrusion Detection Tool
• TVOC: A Translation Validator for Optimizing Compilers
• Cogent: Accurate Theorem Proving for Program Verification
• F-Soft: Software Verification Platform
• Decision Procedures and Applications
• Yet Another Decision Procedure for Equality Logic
• DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic
• Efficient Satisfiability Modulo Theories via Delayed Theory Combination
• Automata and Transition Systems
• Symbolic Systems, Explicit Properties: On Hybrid Approaches for LTL Symbolic Model Checking
• Efficient Monitoring of ?-Languages
• Verification of Tree Updates for Optimization
• Expand, Enlarge and Check... Made Efficient
• Tool Papers III
• IIV: An Invisible Invariant Verifier
• Action Language Verifier, Extended
• Romeo: A Tool for Analyzing Time Petri Nets
• TRANSYT:A Tool for the Verification of Asynchronous Concurrent Systems
• Ymer: A Statistical Model Checker
• Program Analysis and Verification I
• Extended Weighted Pushdown Systems
• Incremental Algorithms for Inter-procedural Analysis of Safety Properties
• A Policy Iteration Algorithm for Computing Fixed Points in Static Analysis of Programs
• Program Analysis and Verification II
• Data Structure Specifications via Local Equality Axioms
• Linear Ranking with Reachability
• Reasoning About Threads Communicating via Locks
• Applications of Learning
• Abstraction Refinement via Inductive Learning
• Automated Assume-Guarantee Reasoning for Simulation Conformance
• Symbolic Compositional Verification by Learning Assumptions.