4. VMCAI 2003: New York, NY, USA

Lenore D. Zuck, Paul C. Attie, Agostino Cortesi, Supratik Mukhopadhyay (Eds.): Verification, Model Checking, and Abstract Interpretation, 4th International Conference, VMCAI 2003, New York, NY, USA, January 9-11, 2002, Proceedings. Lecture Notes in Computer Science 2575 Springer 2003, ISBN 3-540-00348-7

Invited Talks

Andreas Podelski:
Software Model Checking with Abstraction Refinement. 1-3
Amir Pnueli, Lenore D. Zuck:
Model-Checking and Abstraction to the Aid of Parameterized Systems. 4

Invited Tutorials

Bernhard Steffen, Hardi Hungar:
Behavior-Based Model Construction. 5-19
Patrick Cousot:
Automatic Verification by Abstract Interpretation. 20-24
A. Prasad Sistla:
Symmetry Reductions in Model-Checking. 25

Static Analysis

Néstor Cataño, Marieke Huisman:
CHASE: A Static Checker for JML's Assignable Clause. 26-40
Xavier Rival:
Abstract Interpretation-Based Certification of Assembly Code. 41-55
Damien Massé:
Property Checking Driven Abstract Interpretation-Based Static Analysis. 56-69
Leena Unnikrishnan, Scott D. Stoller, Yanhong A. Liu:
Optimized Live Heap Bound Analysis. 70-85

Dynamic Systems

Chiara Braghin, Agostino Cortesi, Riccardo Focardi, Flaminia L. Luccio, Carla Piazza:
Complexity of Nesting Analysis in Mobile Ambients. 86-101
Francesca Levi:
Types for Evolving Communication in Safe Ambients. 102-115
Ping Yang, C. R. Ramakrishnan, Scott A. Smolka:
A Logical Encoding of the pi-Calculus: Model Checking Mobile Processes Using Tabled Resolution. 116-131

Abstract Interpretation

Roberta Gori, Giorgio Levi:
Properties of a Type Abstract Interpreter. 132-145
Roberto Giacobazzi, Isabella Mastroeni:
Domain Compression for Complete Abstractions. 146-160
David Monniaux:
Abstraction of Expectation Functions Using Gaussian Distributions. 161-173

Model Checking I

Kedar S. Namjoshi:
Lifting Temporal Proofs through Abstractions. 174-188
Farn Wang:
Efficient Verification of Timed Automata with BDD-Like Data-Structures. 189-205
Patrice Godefroid, Radha Jagadeesan:
On the Expressiveness of 3-Valued Models. 206-222

Security Protocols

Annalisa Bossi, Riccardo Focardi, Carla Piazza, Sabina Rossi:
Bisimulation and Unwinding for Verifying Possibilistic Security Properties. 223-237
Kazuhiro Ogata, Kokichi Futatsugi:
Formal Verification of the Horn-Preneel Micropayment Protocol. 238-252

Formal Methods

Mila E. Majster-Cederbaum, Naijun Zhan, Harald Fecher:
Action Refinement from a Logical Point of View. 253-267
B. Meenakshi, Ramaswamy Ramanujam:
Reasoning about Layered Message Passing Systems. 268-282
Toh Ne Win, Michael D. Ernst, Stephen J. Garland, Dilsun Kirli Kaynar, Nancy A. Lynch:
Using Simulated Execution in Verifying Distributed Algorithms. 283-297

Model Checking II

Daniel Kroening, Ofer Strichman:
Efficient Computation of Recurrence Diameters. 298-309
Dennis Dams, Kedar S. Namjoshi:
Shape Analysis through Predicate Abstraction and Model Checking. 310-324

Last update Tue May 21 01:20:26 2013 CET by the DBLP Team —

This material is Open Data

Data released under the ODC-BY 1.0 license — See also our legal information page