Verification, Model Checking, and Abstract Interpretation 4th International Conference, VMCAI 2003, New York, NY, USA, January 9-11, 2003, Proceedings /

• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Άλλοι συγγραφείς: Zuck, Lenore D. (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt), Attie, Paul D. (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt), Cortesi, Agostino (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt), Mukhopadhyay, Supratik (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2003.
• Έκδοση: 1st ed. 2003.
• Σειρά: Lecture Notes in Computer Science, 2575
• Θέματα: Software engineering.; Computer logic.; Programming languages (Electronic computers).; Software Engineering.; Logics and Meanings of Programs.; Programming Languages, Compilers, Interpreters.

This volume contains the proceedings of the 4th International Conference on Veri?cation, Model Checking, and Abstract Interpretation (VMCAI 2003), held in New York city, January 9-11, 2003. The purpose of VMCAI was to provide a forum for researchers from three communities-Veri?cation, Model Checking...

Πίνακας περιεχομένων:

• Invited Talks
• Software Model Checking with Abstraction Refinement
• Model-Checking and Abstraction to the Aid of Parameterized Systems
• Invited Tutorials
• Behavior-Based Model Construction
• Automatic Verification by Abstract Interpretation
• Symmetry Reductions in Model-Checking
• Static Analysis
• CHASE:A Static Checker for JML's Assignable Clause
• Abstract Interpretation-Based Certification of Assembly Code
• Property Checking Driven Abstract Interpretation-Based Static Analysis
• Optimized Live Heap Bound Analysis
• Dynamic Systems
• Complexity of Nesting Analysis in Mobile Ambients
• Types for Evolving Communication in Safe Ambients
• A Logical Encoding of the ?-Calculus: Model Checking Mobile Processes Using Tabled Resolution
• Abstract Interpretation
• Properties of a Type Abstract Interpreter
• Domain Compression for Complete Abstractions
• Abstraction of Expectation Functions Using Gaussian Distributions
• Model Checking I
• Lifting Temporal Proofs through Abstractions
• Efficient Verification of Timed Automata with BDD-Like Data-Structures
• On the Expressiveness of 3-Valued Models
• Security Protocols
• Bisimulation and Unwinding for Verifying Possibilistic Security Properties
• Formal Verification of the Horn-Preneel Micropayment Protocol
• Formal Methods
• Action Refinement from a Logical Point of View
• Reasoning about Layered Message Passing Systems
• Using Simulated Execution in Verifying Distributed Algorithms
• Model Checking II
• Efficient Computation of Recurrence Diameters
• Shape Analysis through Predicate Abstraction and Model Checking.