Verification, Model Checking, and Abstract Interpretation: 11th International Conference, VMCAI 2010, Madrid, Spain, January 17-19, 2010, Proceedings

Front Cover
Springer Science & Business Media, Jan 8, 2010 - Computers - 397 pages
This volume contains the proceedings of the 11th International Conference on Veri?cation, Model Checking, and Abstract Interpretation (VMCAI 2010), held in Madrid, Spain, January 17–19, 2010. VMCAI 2010 was the 11th in a series of meetings. Previous meetings were held in Port Je?erson (1997), Pisa (1998), Venice (2002), New York (2003), Venice(2004),Paris(2005),Charleston(2006),Nice(2007),SanFrancisco(2008), and Savannah (2009). VMCAI centers on state-of-the-art research relevant to analysis of programs and systems and drawn from three research communities: veri?cation, model checking, and abstract interpretation. A goal is to facilitate interaction, cro- fertilization, and the advance of hybrid methods that combine two or all three areas. Topics covered by VMCAI include program veri?cation, program cert- cation, model checking, debugging techniques, abstract interpretation, abstract domains, static analysis, type systems, deductive methods, and optimization. The Program Committee selected 21 papers out of 57 submissions based on anonymous reviews and discussions in an electronic Program Committee me- ing. The principal selection criteria were relevance and quality.
 

What people are saying - Write a review

We haven't found any reviews in the usual places.

Contents

Analysis of Systems with Stochastic Process Creation
1
Verifying Concurrent Programs with Chalice
2
Static Timing Analysis for Hard RealTime Systems
3
Abstract InterpretationBased Protection
23
Advances in Probabilistic Model Checking
25
Building a Calculus of Data Structures
26
Temporal Reasoning for Procedural Programs
45
Improved Model Checking of Hierarchical Systems
61
Automatic Abstraction for Congruences
197
Shape Analysis of LowLevel C with Overlapping Structures
214
Abstract Threads
231
Shape Analysis with Reference Set Relations
247
Shape Analysis in the Absence of Pointers and Structure
263
An Analysis of Permutations in Arrays
279
Regular Linear Temporal Logic with Past
295
ModelChecking InLined Reference Monitors
312

PathOriented Reachability Verification of a Class of Nonlinear Hybrid Automata Using Convex Programming
78
Complexity Bounds for the Verification of RealTime Software
95
An Abstract Domain to Discover Interval Linear Equalities
112
Interpolant Strength
129
Checking Bounded Reachability in Asynchronous Systems by Symbolic Event Tracing
146
Invariant and Type Inference for Matrices
163
Deriving Invariants by Algorithmic Learning Decision Procedures and Predicate Abstraction
180
Considerate Reasoning and the Composite Design Pattern
328
RGSep Action Inference
345
Best Probabilistic Transformers
362
Collections Cardinalities and Relations
380
Author Index
396
Copyright

Other editions - View all

Common terms and phrases

Bibliographic information