Verification, Model Checking, and Abstract Interpretation 6th International Conference, VMCAI 2005, Paris, France, January 17-19, 2005. Proceedings /

Λεπτομέρειες βιβλιογραφικής εγγραφής
Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
Άλλοι συγγραφείς: Cousot, Radhia (Επιμελητής έκδοσης)
Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
Γλώσσα: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.