Verification, model checking, and abstract interpretation 6th international conference, VMCAI 2005, Paris, France, January 17-19, 2005 : proceedings
Autor Corporativo: | |
---|---|
Otros Autores: | |
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.