Zur Zeit liegt uns keine Inhaltsangabe vor.
Inhaltsverzeichnis
Invited Paper. - Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming. - Numerical 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. - Invited Talk. - The Verifying Compiler, a Grand Challenge for Computing Research. - Verification 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 Refinement. - Invited Talk. - Abstraction for Liveness. - Heap 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 Programs. - Abstract Model Checking. - Automata as Abstractions. - Don t Know in the ? -Calculus. - Model Checking of Systems Employing Commutative Functions. - Model 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 Checking. - Applied Abstract Interpretation. - Verification of an Error Correcting Code by Abstract Interpretation. - Information Flow Analysis for Java Bytecode. - Cryptographic Protocol Analysis on Real C Code. - Bounded Model Checking. - Simple Is Better: Efficient Bounded Model Checking for Past LTL. - Optimizing Bounded Model Checking for Linear HybridSystems. - Verification II. - Efficient Verification of Halting Properties for MPI Programs with Wildcard Receives. - Generalized Typestate Checking for Data Structure Consistency. - On the Complexity of Error Explanation. - Efficiently Verifiable Conditions for Deadlock-Freedom of Large Concurrent Programs.