Lenore D. Zuck, Paul C. Attie, Agostino Cortesi, Supratik Mukhopadhyay
Proceedings of the Fourth International Conference on Verification, Model Checking and Abstract Interpretation
VMCAI, 2003.

@proceedings{VMCAI-2003,
	address       = "New York, New York, USA",
	editor        = "Lenore D. Zuck and Paul C. Attie and Agostino Cortesi and Supratik Mukhopadhyay",
	isbn          = "3-540-00348-7",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the Fourth International Conference on Verification, Model Checking and Abstract Interpretation}",
	volume        = 2575,
	year          = 2003,
}

Contents (25 items)

6 ×#abstraction
5 ×#model checking
5 ×#verification
3 ×#abstract interpretation
3 ×#analysis
3 ×#using
2 ×#logic
2 ×#mobile
2 ×#performance
2 ×#refinement

VMCAI-2003-Podelski #abstraction #model checking #refinement

Software Model Checking with Abstraction Refinement (AP), pp. 1–3.

VMCAI-2003-PnueliZ #abstraction #model checking

Model-Checking and Abstraction to the Aid of Parameterized Systems (AP, LDZ), p. 4.

VMCAI-2003-SteffenH #behaviour

Behavior-Based Model Construction (BS, HH), pp. 5–19.

VMCAI-2003-Cousot #abstract interpretation #automation #verification

Automatic Verification by Abstract Interpretation (PC), pp. 20–24.

VMCAI-2003-Sistla #model checking #reduction #symmetry

Symmetry Reductions in Model-Checking (APS), p. 25.

VMCAI-2003-CatanoH #ml #named #static analysis

CHASE: A Static Checker for JML’s Assignable Clause (NC, MH), pp. 26–40.

VMCAI-2003-Rival #abstract interpretation #assembly #certification

Abstract Interpretation-Based Certification of Assembly Code (XR), pp. 41–55.

VMCAI-2003-Masse #abstract interpretation #static analysis

Property Checking Driven Abstract Interpretation-Based Static Analysis (DM), pp. 56–69.

VMCAI-2003-UnnikrishnanSL #analysis #bound

Optimized Live Heap Bound Analysis (LU, SDS, YAL), pp. 70–85.

VMCAI-2003-BraghinCFLP #analysis #complexity #mobile

Complexity of Nesting Analysis in Mobile Ambients (CB, AC, RF, FLL, CP), pp. 86–101.

VMCAI-2003-Levi #communication #evolution

Types for Evolving Communication in Safe Ambients (FL), pp. 102–115.

VMCAI-2003-YangRS #encoding #logic #mobile #model checking #process #using #π-calculus

A Logical Encoding of the pi-Calculus: Model Checking Mobile Processes Using Tabled Resolution (PY, CRR, SAS), pp. 116–131.

VMCAI-2003-GoriL #interpreter

Properties of a Type Abstract Interpreter (RG, GL), pp. 132–145.

VMCAI-2003-GiacobazziM #abstraction

Domain Compression for Complete Abstractions (RG, IM), pp. 146–160.

VMCAI-2003-Monniaux #abstraction #using

Abstraction of Expectation Functions Using Gaussian Distributions (DM), pp. 161–173.

VMCAI-2003-Namjoshi #abstraction #proving

Lifting Temporal Proofs through Abstractions (KSN), pp. 174–188.

VMCAI-2003-Wang #automaton #performance #verification

Efficient Verification of Timed Automata with BDD-Like Data-Structures (FW), pp. 189–205.

VMCAI-2003-GodefroidJ #modelling #on the

On the Expressiveness of 3-Valued Models (PG, RJ), pp. 206–222.

VMCAI-2003-BossiFPR #bisimulation #security #verification

Bisimulation and Unwinding for Verifying Possibilistic Security Properties (AB, RF, CP, SR), pp. 223–237.

VMCAI-2003-OgataF #protocol #verification

Formal Verification of the Horn-Preneel Micropayment Protocol (KO, KF), pp. 238–252.

VMCAI-2003-Majster-CederbaumZF #logic #perspective #refinement

Action Refinement from a Logical Point of View (MEMC, NZ, HF), pp. 253–267.

VMCAI-2003-MeenakshiR #message passing #reasoning

Reasoning about Layered Message Passing Systems (BM, RR), pp. 268–282.

VMCAI-2003-WinEGKL #algorithm #distributed #execution #using #verification

Using Simulated Execution in Verifying Distributed Algorithms (TNW, MDE, SJG, DKK, NAL), pp. 283–297.

VMCAI-2003-KroeningS #performance

Efficient Computation of Recurrence Diameters (DK, OS), pp. 298–309.

VMCAI-2003-DamsN #abstraction #analysis #model checking

Shape Analysis through Predicate Abstraction and Model Checking (DD, KSN), pp. 310–324.