Computer Aided Verification : 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014, Proceedings / edited by Armin Biere, Roderick Bloem.

Format:

Book

Contributor:

Biere, Armin, editor.

Bloem, Roderick, editor.

SpringerLink (Online service)

Series:

Computer Science (Springer-11645)

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

Theoretical Computer Science and General Issues ; 8559

Language:

English

Subjects (All):

Computer logic.

Software engineering.

Logic, Symbolic and mathematical.

Computer organization.

Logics and Meanings of Programs.

Software Engineering/Programming and Operating Systems.

Mathematical Logic and Formal Languages.

Computer Systems Organization and Communication Networks.

Local Subjects:

Logics and Meanings of Programs.

Software Engineering/Programming and Operating Systems.

Mathematical Logic and Formal Languages.

Computer Systems Organization and Communication Networks.

Physical Description:

1 online resource (XXXIV, 877 pages) : 205 illustrations.

Edition:

First edition 2014.

Contained In:

Springer eBooks

Place of Publication:

Cham : Springer International Publishing : Imprint: Springer, 2014.

System Details:

text file PDF

Summary:

This book constitutes the proceedings of the 26th International Conference on Computer Aided Verification, CAV 2014, held as part of the Vienna Summer of Logic, VSL 2014, in Vienna, Austria, in July 2014. The 46 regular papers and 11 short papers presented in this volume were carefully reviewed and selected from a total of 175 regular and 54 short paper submissions. The contributions are organized in topical sections named: software verification; automata; model checking and testing; biology and hybrid systems; games and synthesis; concurrency; SMT and theorem proving; bounds and termination; and abstraction.

Contents:

Software Verification

The Spirit of Ghost Code

SMT-Based Model Checking for Recursive Programs

Property-Directed Shape Analysis

Shape Analysis via Second-Order Bi-Abduction

ICE: A Robust Framework for Learning Invariants

From Invariant Checking to Invariant Inference Using Randomized Search

SMACK: Decoupling Source Language Details from Verifier Implementations

Security

Synthesis of Masking Countermeasures against Side Channel Attacks

Temporal Mode-Checking for Runtime Monitoring of Privacy Policies

String Constraints for Verification

A Conference Management System with Verified Document Confidentiality

VAC - Verifier of Administrative Role-Based Access Control Policies

Automata

From LTL to Deterministic Automata: A Safraless Compositional Approach

Symbolic Visibly Pushdown Automata

Model Checking and Testing

Engineering a Static Verification Tool for GPU Kernels

Lazy Annotation Revisited

Interpolating Property Directed Reachability

Verifying Relative Error Bounds Using Symbolic Simulation

Regression Test Selection for Distributed Software Histories

GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components

Software Verification in the Google App-Engine Cloud

The nuXmv Symbolic Model Checker

Biology and Hybrid Systems Analyzing and Synthesizing Genomic Logic Functions

Finding Instability in Biological Models

Invariant Verification of Nonlinear Hybrid Automata Networks of Cardiac Cells

Diamonds Are a Girl's Best Friend: Partial Order Reduction for Timed Automata with Abstractions

Reachability Analysis of Hybrid Systems Using Symbolic Orthogonal Projections

Verifying LTL Properties of Hybrid Systems with K-Liveness

Games and Synthesis

Safraless Synthesis for Epistemic Temporal Specifications

Minimizing Running Costs in Consumption Systems

CEGAR for Qualitative Analysis of Probabilistic Systems

Optimal Guard Synthesis for Memory Safety

Don't Sit on the Fence: A Static Analysis Approach to Automatic Fence Insertion

MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications

Solving Games without Controllable Predecessor

G4LTL-ST: Automatic Generation of PLC Programs

Concurrency

Automatic Atomicity Verification for Clients of Concurrent Data Structures

Regression-Free Synthesis for Concurrency

Bounded Model Checking of Multi-threaded C Programs via Lazy Sequentialization

An SMT-Based Approach to Coverability Analysis

LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes

SMT and Theorem Proving

Monadic Decomposition

A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions

Bit-Vector Rewriting with Automatic Rule Generation

A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors

AVATAR: The Architecture for First-Order Theorem Provers

Automating Separation Logic with Trees and Data

A Nonlinear Real Arithmetic Fragment

Yices 2.2

Bounds and Termination

A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis

Symbolic Resource Bound Inference for Functional Programs

Proving Non-termination Using Max-SMT

Termination Analysis by Learning Terminating Programs

Causal Termination of Multi-threaded Programs

Abstraction

Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR)

Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction

QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers.

Other Format:

Printed edition:

ISBN:

978-3-319-08867-9

9783319088679

Access Restriction:

Restricted for use by site license.