Verification, Model Checking, and Abstract Interpretation 6th International Conference, VMCAI 2005, Paris, France, January 17-19, 2005. Proceedings /
Συγγραφή απο Οργανισμό/Αρχή: | |
---|---|
Άλλοι συγγραφείς: | |
Μορφή: | Ηλεκτρονική πηγή Ηλ. βιβλίο |
Γλώσσα: | English |
Έκδοση: |
Berlin, Heidelberg :
Springer Berlin Heidelberg,
2005.
|
Σειρά: | Lecture Notes in Computer Science,
3385 |
Θέματα: | |
Διαθέσιμο Online: | Full Text via HEAL-Link |
Πίνακας περιεχομένων:
- 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 Hybrid Systems
- 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.