Agostino Cortesi
Proceedings of the Third International Workshop on Verification, Model Checking and Abstract Interpretation
VMCAI, 2002.

@proceedings{VMCAI-2002,
	address       = "Venice, Italy",
	editor        = "Agostino Cortesi",
	isbn          = "3-540-43631-6",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the Third International Workshop on Verification, Model Checking and Abstract Interpretation}",
	volume        = 2294,
	year          = 2002,
}

Contents (22 items)

4 ×#model checking
4 ×#verification
2 ×#abstract interpretation
2 ×#analysis
2 ×#game studies
2 ×#protocol
2 ×#security
2 ×#termination

VMCAI-2002-BernardeschiF #abstract interpretation #bytecode #java #model checking #security

Combining Abstract Interpretation and Model Checking for Analysing Security Properties of Java Bytecode (CB, NDF), pp. 1–15.

VMCAI-2002-FocardiPR #bisimulation #data flow #proving #security

Proofs Methods for Bisimulation Based Information Flow Security (RF, CP, SR), pp. 16–31.

VMCAI-2002-BartheDJS #virtual machine

A Formal Correspondence between Offensive and Defensive JavaCard Virtual Machines (GB, GD, LJ, SMdS), pp. 32–45.

VMCAI-2002-Shyamasundar #encryption #framework #protocol

Analyzing Cryptographic Protocols in a Reactive Framework (RKS), pp. 46–64.

VMCAI-2002-Tan #game studies

An Abstract Schema for Equivalence-Checking Games (LT), pp. 65–78.

VMCAI-2002-SidorovaS #model checking

Synchronous Closing of Timed SDL Systems for Model Checking (NS, MS), pp. 79–93.

VMCAI-2002-FaellaTM #game studies

Automata-Theoretic Decision of Timed Games (MF, SLT, AM), pp. 94–108.

VMCAI-2002-CharatonikMP #analysis #composition #termination

Compositional Termination Analysis of Symbolic Forward Analysis (WC, SM, AP), pp. 109–125.

VMCAI-2002-GenaimCGL #termination

Combining Norms to Prove Termination (SG, MC, JPG, VL), pp. 126–138.

VMCAI-2002-MurawskiY #analysis

Static Monotonicity Analysis for lambda-definable Functions over Lattices (ASM, KY), pp. 139–153.

VMCAI-2002-HillS #refinement

A Refinement of the Escape Property (PMH, FS), pp. 154–166.

VMCAI-2002-TronconBJC #array #reduction

Storage Size Reduction by In-place Mapping of Arrays (RT, MB, GJ, FC), pp. 167–181.

VMCAI-2002-KrsticM #algorithm #monad #verification

Verifying BDD Algorithms through Monadic Interpretation (SK, JM), pp. 182–195.

VMCAI-2002-CimattiPRS #encoding #ltl #model checking #satisfiability

Improving the Encoding of LTL Model Checking into SAT (AC, MP, MR, RS), pp. 196–207.

VMCAI-2002-ZuckPK #automation #probability #verification

Automatic Verification of Probabilistic Free Choice (LDZ, AP, YK), pp. 208–224.

VMCAI-2002-GoriL #abstract interpretation #empirical #type inference #verification

An Experiment in Type Inference and Verification by Abstract Interpretation (RG, GL), pp. 225–239.

VMCAI-2002-TorreMN #automaton

Weak Muller Acceptance Conditions for Tree Automata (SLT, AM, MN), pp. 240–254.

VMCAI-2002-CoppoD #higher-order #mobile

A Fully Abstract Model for Higher-Order Mobile Ambients (MC, MDC), pp. 255–271.

VMCAI-2002-TipleaT #abstraction #simulation

A Simulation Preorder for Abstraction of Reactive Systems (FLT, AT), pp. 272–288.

VMCAI-2002-HardingRS #approximate #atl

Approximating ATL* in ATL (AH, MR, PYS), pp. 289–301.

VMCAI-2002-Huth #model checking #using

Model Checking Modal Transition Systems Using Kripke Structures (MH), pp. 302–316.

VMCAI-2002-BaukusLS #liveness #protocol #safety #verification

Parameterized Verification of a Cache Coherence Protocol: Safety and Liveness (KB, YL, KS), pp. 317–330.