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.
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.
