Verification, Model Checking, and Abstract Interpretation: 4th International Conference, Vmcai 2003, New York, Ny, Usa, January 2003 : Proceedings

by Zuck, Lenore D.; Attie, Paul C.; Cortesi, Agostino; Mukhopadhyay, Supratik; Vmcai 200 (2003 New York, Ny)

• ISBN13: 9783540003489
• ISBN10: 3540003487
• Format: Paperback
• Copyright: 2003-01-01
• Publisher: Springer Verlag

Summary

This book constitutes the refereed proceedings of the 4th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2003, held in New York, NY, USA in January 2003. The 20 revised full papers presented together with five invited contributions were carefully reviewed and selected from 43 submissions. The papers are organized in topical sections on static analysis, dynamic systems, abstract interpretation, model checking, security protocols, and formal methods.

Table of Contents

Invited Talks
Software Model Checking with Abstraction Refinement	1	(3)
Andreas Podelski
Model-Checking and Abstraction to the Aid of Parameterized Systems	4	(1)
Amir Pnueli, Lenore Zuck
Invited Tutorials
Behavior-Based Model Construction	5	(15)
Bernhard Steffen, Hardi Hungar
Automatic Verification by Abstract Interpretation	20	(5)
Patrick Cousot
Symmetry Reductions in Model-Checking	25	(1)
Aravinda Prasad Sistla
Static Analysis
CHASE: A Static Checker for JML's Assignable Clause	26	(15)
Néstor Cataño, Marieke Huisman
Abstract Interpretation-Based Certification of Assembly Code	41	(15)
Xavier Rival
Property Checking Driven Abstract Interpretation-Based Static Analysis	56	(14)
Damien Massé
Optimized Live Heap Bound Analysis	70	(16)
Leena Unnikrishnan, Scott D. Stoller, Yanhong A. Liu
Dynamic Systems
Complexity of Nesting Analysis in Mobile Ambients	86	(16)
Chiara Braghin, Agostino Cortesi, Riccardo Focardi, Flaminia L. Luccio, Carla Piazza
Types for Evolving Communication in Safe Ambients	102	(14)
Francesca Levi
A Logical Encoding of the it-Calculus: Model Checking Mobile Processes Using Tabled Resolution	116	(16)
Ping Yang, C.R. Ramakrishnan, Scott A. Smolka
Abstract Interpretation
Properties of a Type Abstract Interpreter	132	(14)
Roberta Gori, Giorgio Levi
Domain Compression for Complete Abstractions	146	(15)
Roberto Giacobazzi, Isabella Mastroeni
Abstraction of Expectation Functions Using Gaussian Distributions	161	(13)
David Monniaux
Model Checking I
Lifting Temporal Proofs through Abstractions	174	(15)
Kedar S. Namjoshi
Efficient Verification of Timed Automata with BDD-Like Data-Structures	189	(17)
Farn Wang
On the Expressiveness of 3-Valued Models	206	(17)
Patrice Godefrod, Radha Jagadeesan
Security Protocols
Bisimulation and Unwinding for Verifying Possibilistic Security Properties	223	(15)
Annalisa Bossi, Riccardo Focardi, Carla Piazza, Sabina Rossi
Formal Verification of the Horn-Preneel Micropayment Protocol	238	(15)
Kazuhiro Ogata, Kokichi Futatsugi
Formal Methods
Action Refinement from a Logical Point of View	253	(15)
Mila Majster-Cederbaum, Naijun Zhan, Harald Fecher
Reasoning about Layered Message Passing Systems	268	(15)
B. Meenakshi, R. Ramanujam
Using Simulated Execution in Verifying Distributed Algorithms	283	(15)
Toh Ne Win, Michael D. Ernst, Stephen J. Garland, Dilsun Kirh, Nancy A. Lynch
Model Checking II
Efficient Computation of Recurrence Diameters	298	(12)
Daniel Kroening, Ofer Strichman
Shape Analysis through Predicate Abstraction and Model Checking	310	(15)
Dennis Dams, Kedar S. Namjoshi
Author Index	325