Computer Aided Verification : 20th International Conference, CAV 2008 Princeton, NJ, USA, July 7-14, 2008, Proceedings / edited by Aarti Gupta, Sharad Malik.

Format:

Book

Contributor:

Gupta, Aarti, editor.

Malik, Sharad, editor.

SpringerLink (Online service)

Series:

Computer Science (Springer-11645)

LNCS sublibrary. Theoretical computer science and general issues ; SL 1, 5123.

Theoretical Computer Science and General Issues ; 5123

Language:

English

Subjects (All):

Computer programming.

Computer architecture.

Computer logic.

Software engineering.

Logic, Symbolic and mathematical.

Artificial intelligence.

Programming Techniques.

Computer System Implementation.

Logics and Meanings of Programs.

Software Engineering.

Mathematical Logic and Formal Languages.

Artificial Intelligence.

Local Subjects:

Programming Techniques.

Computer System Implementation.

Logics and Meanings of Programs.

Software Engineering.

Mathematical Logic and Formal Languages.

Artificial Intelligence.

Physical Description:

1 online resource (XVII, 558 pages).

Edition:

First edition 2008.

Contained In:

Springer eBooks

Place of Publication:

Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2008.

System Details:

text file PDF

Summary:

This book constitutes the refereed proceedings of the 20th International Conference on Computer Aided Verification, CAV 2008, held in Princeton, NJ, USA, in July 2008. The 33 revised full papers presented together with 14 tool papers and 2 invited papers and 4 invited tutorials were carefully reviewed and selected from 104 regular paper and 27 tool paper submissions. The papers are organized in topical sections on concurrency, memory consistency, abstraction/refinement, hybrid systems, dynamic verification, modeling and specification formalisms, decision procedures, program verification, program and shape analysis, security and program analysis, hardware verification, model checking, space efficient algorithms, and model checking.

Contents:

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?.

Other Format:

Printed edition:

ISBN:

978-3-540-70545-1

9783540705451

Access Restriction:

Restricted for use by site license.