Verification, Model Checking, and Abstract Interpretation 验证、模型检验与抽象解释/会议录

作者简介

The book constitutes the refereed proceedings of the 6th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2005, held in Paris, France in January 2005.    The 27 revised full papers presented together with an invited paper were carefully reviewed and selected from 92 submissions. The papers are organized in topical sections on numerical abstraction, verification, heap and shape analysis, abstract model checking, model checking, applied abstract interpretation, and bounded model checking.

书籍目录

Invited Paper　Proving Program Invariance and Termination by Parametric Abstraction,　Lagrangian Relaxation and Semidefinite ProgrammingNumerical Abstraction　Scalable Analysis of Linear Systems Using Mathematical Programming　The Arithmetic-Geometric Progression Abstract Domain　An Overview of Semantics for the Validation of Numerical Programs   Matthieu MartelInvited Talk　The Verifying Compiler, a Grand Challenge for Computing ResearchVerification I　Checking Herbrand Equalities and Beyond　Static Analysis by Abstract Interpretation　of the Quasi-synchronous Composition of Synchronous Programs　Termination of Polynomial Programs　Verifying Safety of a Token Coherence Implementation　by Parametric Compositional RefinementInvited Talk　Abstraction for LivenessHeap and Shape Analysis　Abstract Interpretation with Alien Expressions and Heap Structures　Shape Analysis by Predicate Abstraction　Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists..　Purity and Side Effect Analysis for Java ProgramsAbstract Model Checking　Automata as Abstractions　Don't Know in the #-Calculus　Model Checking of Systems Employing Commutative FunctionsModel Checking　Weak Automata for the Linear Time #-Calculus　Model Checking for Process Rewrite Systems　and a Class of Action-Based Regular Properties　Minimizing Counterexample with Unit Core Extraction　and Incremental SAT　I/O Efficient Directed Model CheckingApplied Abstract Interpretation　Verification of an Error Correcting Code by Abstract Interpretation　Information Flow Analysis for Java Bytecode　Cryptographic Protocol Analysis on Real C CodeBounded Model CheckingVerfication IIAuthor Index

 Verification, Model Checking, and Abstract Interpretation 验证、模型检验与抽象解释/会议录下载