Computer Aided Verification 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007. Proceedings /

• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Άλλοι συγγραφείς: Damm, Werner (Επιμελητής έκδοσης), Hermanns, Holger (Επιμελητής έκδοσης)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg, 2007.
• Σειρά: Lecture Notes in Computer Science, 4590
• Θέματα: Computer science.; Logic design.; Software engineering.; Computers.; Computer logic.; Mathematical logic.; Artificial intelligence.; Computer Science.; Theory of Computation.; 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 C- puter Aided Veri?cation (CAV), held in Berlin, Germany, July 3–7, 2007. CAV 2007 was the 19th in a series of conferences dedicated to the advancement of the theory and practice of computer-assisted formal analysis methods for...

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

• Invited Talks
• Automatically Proving Program Termination
• A Mathematical Approach to RTL Verification
• Software Bugs Seen from an Industrial Perspective or Can Formal Methods Help on Automotive Software Development?
• Invited Tutorials
• Algorithms for Interface Synthesis
• A Tutorial on Satisfiability Modulo Theories
• A JML Tutorial: Modular Specification and Verification of Functional Behavior for Java
• Verification of Hybrid Systems
• Session I: Compositionality
• SAT-Based Compositional Verification Using Lazy Learning
• Local Proofs for Global Safety Properties
• Session II: Verification Process
• Low-Level Library Analysis and Summarization
• Verification Across Intellectual Property Boundaries
• Session III: Timed Synthesis and Games
• On Synthesizing Controllers from Bounded-Response Properties
• An Accelerated Algorithm for 3-Color Parity Games with an Application to Timed Games
• UPPAAL-Tiga: Time for Playing Games!
• The TASM Toolset: Specification, Simulation, and Formal Verification of Real-Time Systems
• Session IV: Infinitive State Verification
• Systematic Acceleration in Regular Model Checking
• Parameterized Verification of Infinite-State Processes with Global Conditions
• Session V: Tool Environment
• CADP 2006: A Toolbox for the Construction and Analysis of Distributed Processes
• jMoped: A Test Environment for Java Programs
• Hector: Software Model Checking with Cooperating Analysis Plugins
• The Why/Krakatoa/Caduceus Platform for Deductive Program Verification
• Session VI: Shapes
• Shape Analysis for Composite Data Structures
• Array Abstractions from Proofs
• Context-Bounded Analysis of Multithreaded Programs with Dynamic Linked Structures
• Revamping TVLA: Making Parametric Shape Analysis Competitive
• Session VII: Concurrent Program Verification
• Fast and Accurate Static Data-Race Detection for Concurrent Programs
• Parametric and Sliced Causality
• Spade: Verification of Multithreaded Dynamic and Recursive Programs
• Session VIII: Reactive Designs
• Anzu: A Tool for Property Synthesis
• RAT: A Tool for the Formal Analysis of Requirements
• Session IX: Parallelisation
• Parallelising Symbolic State-Space Generators
• I/O Efficient Accepting Cycle Detection
• Session X: Constraints and Decisions
• C32SAT: Checking C Expressions
• CVC3
• BAT: The Bit-Level Analysis Tool
• LIRA: Handling Constraints of Linear Arithmetics over the Integers and the Reals
• Session XI: Probabilistic Verification
• Three-Valued Abstraction for Continuous-Time Markov Chains
• Magnifying-Lens Abstraction for Markov Decision Processes
• Underapproximation for Model-Checking Based on Random Cryptographic Constructions
• Session XII: Abstraction
• Using Counterexamples for Improving the Precision of Reachability Computation with Polyhedra
• Structural Abstraction of Software Verification Conditions
• An Abstract Domain for Analyzing Heap-Manipulating Low-Level Software
• Adaptive Symmetry Reduction
• Session XIII: Assume-Guarantee Reasoning
• From Liveness to Promptness
• Automated Assumption Generation for Compositional Verification
• Session XIV: Hybrid Systems
• Abstraction and Counterexample-Guided Construction of ?-Automata for Model Checking of Step-Discrete Linear Hybrid Models
• Test Coverage for Continuous and Hybrid Systems
• Hybrid Systems: From Verification to Falsification
• Session XV: Program Analysis
• Comparison Under Abstraction for Verifying Linearizability
• Leaping Loops in the Presence of Abstraction
• Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis
• Session XVI: SAT and Decision Procedures
• A Decision Procedure for Bit-Vectors and Arrays
• Boolean Abstraction for Temporal Logic Satisfiability
• A Lazy and Layered SMT( ) Solver for Hard Industrial Verification Problems.