Verification, model checking, and abstract interpretation 6th international conference, VMCAI 2005, Paris, France, January 17-19, 2005 : proceedings

Detalles Bibliográficos
Autor Corporativo: VMCAI 2005 (-)
Otros Autores: Cousot, Radhia (-)
Formato: Libro electrónico
Idioma:Inglés
Publicado: Berlin ; New York : Springer c2005.
Edición:1st ed. 2005.
Colección:Lecture notes in computer science ; 3385.
Materias:
Ver en Biblioteca Universitat Ramon Llull:https://discovery.url.edu/permalink/34CSUC_URL/1im36ta/alma991009713744406719
Tabla de Contenidos:
  • 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.