Computer aided verification : 19th international conference, CAV 2007, Berlin, Germany, July 3-7, 2007 : proceedings, Werner Damm, Holger Hermanns (eds.)

Resource Information

The instance Computer aided verification : 19th international conference, CAV 2007, Berlin, Germany, July 3-7, 2007 : proceedings, Werner Damm, Holger Hermanns (eds.) represents a material embodiment of a distinct intellectual or artistic creation found in University of Missouri Libraries. This resource is a combination of several types including: Instance, Electronic.

Image

http://images.btol.com/ContentCafe/Jacket.aspx?UserID=ebsco-test&Password=ebsco-test&Return=T&Value=9783540733676&Type=L

Label

Computer aided verification : 19th international conference, CAV 2007, Berlin, Germany, July 3-7, 2007 : proceedings, Werner Damm, Holger Hermanns (eds.)

Title remainder

19th international conference, CAV 2007, Berlin, Germany, July 3-7, 2007 : proceedings

Statement of responsibility

Werner Damm, Holger Hermanns (eds.)

Instantiates

• Computer aided verification : 19th international conference, CAV 2007, Berlin, Germany, July 3-7, 2007 : proceedings

Publication

• Berlin | New York, Springer, ©2007

Bibliography note

Includes bibliographical references and index

Carrier category

online resource

Carrier category code

• cr

Carrier MARC source

rdacarrier

Color

multicolored

Content category

text

Content type code

• txt

Content type MARC source

rdacontent

Contents

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

Control code

184907021

Dimensions

unknown

Extent

1 online resource (xv, 562 pages)

Form of item

online

Isbn

9783540733676

Media category

computer

Media MARC source

rdamedia

Media type code

• c

Other control number

10.1007/978-3-540-73368-3

Other physical details

illustrations.

http://library.link/vocab/ext/overdrive/overdriveId

978-3-540-73367-6

Record ID

.b129988480

Specific material designation

remote

System control number

(OCoLC)184907021