a Record control number 014665797

a ISBN 978-354-070545-1

a ISBN 3-540-70545-7

a ISBN 978-354-070543-7

a ISBN 3-540-70543-0

a Original cataloging agency NEU GrandLibrary

a Classification number QA76.76.V47

b Item number .C38 2008

a Dewey Classification 005.14

a Meeting name or jurisdiction name as entry element CAV (Conference)

a Title Computer aided verification :

b Remainder of title 20th international conference, CAV 2008, Princeton, NJ, USA, July 7-14, 2008 : proceedings /

c Statement of responsibility, etc Aarti Gupta, Sharad Malik (eds.).

h Medium BOOK

a Title proper/short title CAV 2008

a Place of publication, distribution, etc Berlin ;

a Place of publication, distribution, etc New York :

b Name of publisher, distributor, etc Springer,

c Date of publication, distribution, etc ©2008.

a Extent 1 online resource (xvii, 558 pages)

a Series statement Lecture notes in computer science,

v Volume number/sequential designation 5123

a Series statement LNCS sublibrary. SL 1, Theoretical computer science and general issues

a Bibliography, etc Includes bibliographical references and index.

a Formatted contents note Invited Talks -- Singularity: Designing Better Software (Invited Talk) -- Coping with Outside-the-Box Attacks -- Invited Tutorials -- Assertion-Based Verification: Industry Myths to Realities (Invited Tutorial) -- Theorem Proving for Verification (Invited Tutorial) -- Tutorial on Separation Logic (Invited Tutorial) -- Abstract Interpretation with Applications to Timing Validation -- Session 1: Concurrency -- Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis -- Monitoring Atomicity in Concurrent Programs -- Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings -- A Hybrid Type System for Lock-Freedom of Mobile Processes -- Session 2: Memory Consistency -- Implied Set Closure and Its Application to Memory Consistency Verification -- Effective Program Verification for Relaxed Memory Models -- Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses -- Session 3: Abstraction/Refinement -- Automated Assume-Guarantee Reasoning by Abstraction Refinement -- Local Proofs for Linear-Time Properties of Concurrent Programs -- Probabilistic CEGAR -- Session 4: Hybrid Systems -- Computing Differential Invariants of Hybrid Systems as Fixedpoints -- Constraint-Based Approach for Analysis of Hybrid Systems -- Session 5: Tools -- Dynamic Verification -- AutoMOTGen: Automatic Model Oriented Test Generator for Embedded Control Systems -- FShell: Systematic Test Case Generation for Dynamic Analysis and Measurement -- Session 6: Modeling and Specification Formalisms -- Applying the Graph Minor Theorem to the Verification of Graph Transformation Systems -- Conflict-Tolerant Features -- Ranking Automata and Games for Prioritized Requirements -- Session 7: Decision Procedures -- Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations -- Linear Arithmetic with Stars -- Inferring Congruence Equations Using SAT -- Session 8: Tools -- Decision Procedures -- The Barcelogic SMT Solver -- The MathSAT 4 SMT Solver -- CSIsat: Interpolation for LA+EUF -- Prover's Palette: A User-Centric Approach to Verification with Isabelle and QEPCAD-B -- Session 9: Program Verification -- Heap Assumptions on Demand -- Proving Conditional Termination -- Monotonic Abstraction for Programs with Dynamic Memory Heaps -- Enhancing Program Verification with Lemmas -- Session 10: Program and Shape Analysis -- A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis -- Scalable Shape Analysis for Systems Code -- Thread Quantification for Concurrent Shape Analysis -- Session 11: Tools -- Security and Program Analysis -- The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols -- The CASPA Tool: Causality-Based Abstraction for Security Protocol Analysis -- Jakstab: A Static Analysis Platform for Binaries -- THOR: A Tool for Reasoning about Shape and Arithmetic -- Session 12: Hardware Verification I -- Functional Verification of Power Gated Designs by Compositional Reasoning -- A Practical Approach to Word Level Model Checking of Industrial Netlists -- Session 13: Hardware Verification II -- Validating High-Level Synthesis -- An Algebraic Approach for Proving Data Correctness in Arithmetic Data Paths -- Application of Formal Word-Level Analysis to Constrained Random Simulation -- Session 14: Model Checking -- Producing Short Counterexamples Using "Crucial Events" -- Discriminative Model Checking -- Session 15: Space Efficient Algorithms -- Correcting a Space-Efficient Simulation Algorithm -- Semi-external LTL Model Checking -- Session 16: Tools -- Model Checking -- QMC: A Model Checker for Quantum Systems -- T(O)RMC: A Tool for -Regular Model Checking -- Faster Than Uppaal?

a Summary, etc Annotation

a Language note English.

a Topical term or geographic name as entry element Computer software

a Topical term or geographic name as entry element Electronic digital computers

a Topical term or geographic name as entry element Informatique.

a Topical term or geographic name as entry element Computer software

a Topical term or geographic name as entry element Electronic digital computers

a Genre/form data or focus term Conference papers and proceedings.

a Personal name Gupta, Aarti,

a Personal name Malik, Sharad.

a Uniform title Lecture notes in computer science ;

a Uniform title LNCS sublibrary.

u Uniform Resource Identifier http://link.springer.com/10.1007/978-3-540-70545-1