Computer Aided Verification

€ 106,99
Lieferbar innerhalb von 2-3 Tagen
Juli 2007



This book constitutes the refereed proceedings of the 19th International Conference on Computer Aided Verification. Thirty-three state-of-the-technology papers are presented, together with fourteen tool papers, three invited papers, and four invited tutorials. All the current issues in computer aided verification and model checking-from foundational and methodological issues to the evaluation of major tools and systems-are addressed.


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.
EAN: 9783540733676
ISBN: 3540733671
Untertitel: 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings. 'Lecture Notes in Computer Science'. 2007. Auflage. Book. Sprache: Englisch.
Verlag: Springer
Erscheinungsdatum: Juli 2007
Seitenanzahl: 584 Seiten
Format: kartoniert
Es gibt zu diesem Artikel noch keine Bewertungen.Kundenbewertung schreiben