Blick ins Buch

Verification, Model Checking, and Abstract Interpretation

10th International Conference, VMCAI 2009, Savannah, GA, USA, January 18-20, 2009. Proceedings

Neil Jones, Markus Müller-Olm (Herausgeber)

Buch | Softcover

XI, 381 Seiten

2008
Springer Berlin (Verlag)
9783540938996 (ISBN)

Lese- und Medienproben

Blick ins Buch (midvox)

Artikel merken

This volume contains the proceedings of the 10th International Conference on Veri?cation, Model Checking, and Abstract Interpretation (VMCAI 2009), held in Savannah, Georgia, USA, January 18-20, 2009. VMCAI 2009 was the 10th in a series of meetings. Previous meetings were heldinPortJe?erson1997,Pisa1998,Venice2002,NewYork2003,Venice2004, Paris 2005, Charleston 2006, Nice 2007, and San Francisco 2008. 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 24 papers out of 72 submissions based on anonymous reviews and discussions in an electronic Program Committee me- ing. The principal selection criteria were relevance and quality. VMCAI has a tradition of inviting distinguished speakers to give talks and tutorials. This time the program included three invited talks by: - E. Allen Emerson (University of Texas at Austin) on "Model Checking: Progress and Problems" - Aarti Gupta (NEC Labs, Princeton) on "Model Checking Concurrent Programs" - Mooly Sagiv (Tel-Aviv University) on "Thread Modular Shape Analysis" There were also two invited tutorials by: - Byron Cook (Microsoft Research, Cambridge) on "Proving Program Ter- nation and Liveness" - V´ eroniqueCortier (LORIA, CNRS, Nancy) on"Veri?cationof Security P- tocols".

Invited Talks.- Model Checking: Progress and Problems.- Model Checking Concurrent Programs.- Thread-Modular Shape Analysis.- Invited Tutorials.- Advances in Program Termination and Liveness.- Verification of Security Protocols.- Submitted Papers.- Towards Automatic Stability Analysis for Rely-Guarantee Proofs.- Mostly-Functional Behavior in Java Programs.- The Higher-Order Aggregate Update Problem.- An Abort-Aware Model of Transactional Programming.- Model-Checking the Linux Virtual File System.- LTL Generalized Model Checking Revisited.- Monitoring the Full Range of ?-Regular Properties of Stochastic Systems.- Constraint-Based Invariant Inference over Predicate Abstraction.- Reducing Behavioural to Structural Properties of Programs with Procedures.- Query-Driven Program Testing.- Average-Price-per-Reward Games on Hybrid Automata with Strong Resets.- Abstraction Refinement for Probabilistic Software.- Finding Concurrency-Related Bugs Using Random Isolation.- An Abstract Interpretation-Based Framework for Control Flow Reconstruction from Binaries.- SubPolyhedra: A (More) Scalable Approach to Infer Linear Inequalities.- Deciding Extensions of the Theories of Vectors and Bags.- A Posteriori Soundness for Non-deterministic Abstract Interpretations.- An Automata-Theoretic Dynamic Completeness Criterion for Bounded Model-Checking.- A Scalable Memory Model for Low-Level Code.- Synthesizing Switching Logic Using Constraint Solving.- Extending Symmetry Reduction by Exploiting System Architecture.- Shape-Value Abstraction for Verifying Linearizability.- Mixed Transition Systems Revisited.- Counterexample Generation for Discrete-Time Markov Chains Using Bounded Model Checking.

Erscheint lt. Verlag	18.12.2008
Reihe/Serie	Lecture Notes in Computer Science
Reihe/Serie	Theoretical Computer Science and General Issues
Zusatzinfo	XI, 381 p.
Verlagsort	Berlin
Sprache	englisch
Maße	155 x 235 mm
Gewicht	605 g
Themenwelt	Mathematik / Informatik ► Informatik ► Betriebssysteme / Server
Themenwelt	Mathematik / Informatik ► Informatik ► Theorie / Studium
Schlagworte	abstract domains • Abstraction • action • debugging techniques • deductive methods • formal methods • Formal Verification • Hardcover, Softcover / Informatik, EDV/Informatik • HC/Informatik, EDV/Informatik • higher-order languages • Model Checking • Optimization • program analysis • program certification • program invariants • programming • programming calculi • Programming language • Program Semantics • program veri • Program verification • Refinement • Static Analysis • structured analysis • Temporal Logics • Type Systems • verification
ISBN-13	9783540938996 / 9783540938996
Zustand	Neuware