Verification, Model Checking, and Abstract Interpretation 8th International Conference, VMCAI 2007, Nice, France, January 14-16, 2007, Proceedings / edited by Byron Cook, Andreas Podelski.

Saved in:

Bibliographic Details
Corporate Author:	SpringerLink (Online service)
Other Authors:	Cook, Byron (Editor), Podelski, Andreas (Editor)
Format:	eBook
Language:	English
Published:	Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2007.
Edition:	1st ed. 2007.
Series:	Theoretical Computer Science and General Issues ; 4349 Springer eBook Collection.
Subjects:	Software engineering. Computer logic. Programming languages (Electronic computers). Electronic resources (E-books)
Online Access:	Click to view e-book
Holy Cross Note:	Loaded electronically. Electronic access restricted to members of the Holy Cross Community.

Table of Contents:

Invited Talk
DIVINE: DIscovering Variables IN Executables
Session 1
Verifying Compensating Transactions
Model Checking Nonblocking MPI Programs
Model Checking Via ?CFA
Using First-Order Theorem Provers in the Jahob Data Structure Verification System
Invited Tutorial
Interpolants and Symbolic Model Checking
Session 2
Shape Analysis of Single-Parent Heaps
An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures
On Flat Programs with Lists
Invited Talk
Automata-Theoretic Model Checking Revisited
Session 3
Language-Based Abstraction Refinement for Hybrid System Verification
More Precise Partition Abstractions
The Spotlight Principle
Lattice Automata
Invited Tutorial
Learning Algorithms and Formal Verification (Invited Tutorial)
Session 4
Constructing Specialized Shape Analyses for Uniform Change
Maintaining Doubly-Linked List Invariants in Shape Analysis with Local Reasoning
Automated Verification of Shape and Size Properties Via Separation Logic
Invited Talk
Towards Shape Analysis for Device Drivers
Session 5
An Abstract Domain Extending Difference-Bound Matrices with Disequality Constraints
Cibai: An Abstract Interpretation-Based Static Analyzer for Modular Analysis and Verification of Java Classes
Symmetry and Completeness in the Analysis of Parameterized Systems
Better Under-Approximation of Programs by Hiding Variables
Invited Tutorial
The Constraint Database Approach to Software Verification
Session 6
Constraint Solving for Interpolation
Assertion Checking Unified
Invariant Synthesis for Combined Theories.

Verification, Model Checking, and Abstract Interpretation 8th International Conference, VMCAI 2007, Nice, France, January 14-16, 2007, Proceedings / edited by Byron Cook, Andreas Podelski.

Similar Items