Bernhard Steffen, Giorgio Levi
Proceedings of the Fifth International Conference on Verification, Model Checking and Abstract Interpretation
VMCAI, 2004.

@proceedings{VMCAI-2004,
	editor        = "Bernhard Steffen and Giorgio Levi",
	isbn          = "3-540-20803-8",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the Fifth International Conference on Verification, Model Checking and Abstract Interpretation}",
	volume        = 2937,
	year          = 2004,
}

Contents (26 items)

6 ×#model checking
3 ×#using
2 ×#abstraction
2 ×#algebra
2 ×#analysis
2 ×#invariant
2 ×#ranking
2 ×#security
2 ×#specification
2 ×#verification

VMCAI-2004-Guttman #protocol #security #trust

Security, Protocols, and Trust (JDG), p. 1.

VMCAI-2004-BartheBR #compilation #security

Security Types Preserving Compilation: (GB, AB, TR), pp. 2–15.

VMCAI-2004-Vanackere #encryption #process #scheduling

History-Dependent Scheduling for Cryptographic Processes (VV), pp. 16–29.

VMCAI-2004-TanASW #assembly #semantics

Construction of a Semantic Model for a Typed Assembly Language (GT, AWA, KNS, DW), pp. 30–43.

VMCAI-2004-BarringerGHS #rule-based #runtime #verification

Rule-Based Runtime Verification (HB, AG, KH, KS), pp. 44–57.

VMCAI-2004-Sagiv #abstraction #canonical #on the #power of

On the Expressive Power of Canonical Abstraction (SS), p. 58.

VMCAI-2004-KuncakR #algebra #analysis #constraints

Boolean Algebra of Shape Analysis Constraints (VK, MCR), pp. 59–72.

VMCAI-2004-HeraultLMP #approximate #model checking #probability

Approximate Probabilistic Model Checking (TH, RL, FM, SP), pp. 73–84.

VMCAI-2004-ClarkeKOS #bound #complexity #model checking

Completeness and Complexity of Bounded Model Checking (EMC, DK, JO, OS), pp. 85–96.

VMCAI-2004-LucanuC #algebra #model checking #specification

Model Checking for Object Specifications in Hidden Algebra (DL, GC), pp. 97–109.

VMCAI-2004-PaceS #difference #kernel #model checking #using

Model Checking Polygonal Differential Inclusions Using Invariance Kernels (GJP, GS), pp. 110–121.

VMCAI-2004-YuX

Checking Interval Based Properties for Reactive Systems (YP, QX), pp. 122–134.

VMCAI-2004-BagnaraHZ #set

Widening Operators for Powerset Domains (RB, PMH, EZ), pp. 135–148.

VMCAI-2004-AgarwalS #java #type inference

Type Inference for Parameterized Race-Free Java (RA, SDS), pp. 149–160.

VMCAI-2004-XiaH #c #source code

Certifying Temporal Properties for Compiled C Programs (SX, JH), pp. 161–174.

VMCAI-2004-HatcliffRD #concurrent #model checking #object-oriented #specification #using #verification

Verifying Atomicity Specifications for Concurrent Object-Oriented Software Using Model-Checking (JH, R, MBD), pp. 175–190.

VMCAI-2004-EnglerM #debugging #model checking #static analysis

Static Analysis versus Software Model Checking for Bug Finding (DRE, MM), pp. 191–210.

VMCAI-2004-Logozzo #automation #invariant

Automatic Inference of Class Invariants (FL), pp. 211–222.

VMCAI-2004-FangPPZ #liveness #ranking

Liveness with Invisible Ranking (YF, NP, AP, LDZ), pp. 223–238.

VMCAI-2004-PodelskiR #linear #ranking #synthesis

A Complete Method for the Synthesis of Linear Ranking Functions (AP, AR), pp. 239–251.

VMCAI-2004-RepsSY #implementation

Symbolic Implementation of the Best Transformer (TWR, SS, GY), pp. 252–266.

VMCAI-2004-LahiriB #abstraction #invariant #quantifier

Constructing Quantified Invariants via Predicate Abstraction (SKL, REB), pp. 267–281.

VMCAI-2004-Etessami #analysis #data flow #equation #game studies #graph #recursion #using

Analysis of Recursive Game Graphs Using Data Flow Equations (KE), pp. 282–296.

VMCAI-2004-ArthoH

Applying Jlint to Space Exploration Software (CA, KH), pp. 297–308.

VMCAI-2004-Wilhelm #why

Why AI + ILP Is Good for WCET, but MC Is Not, Nor ILP Alone (RW), pp. 309–322.

VMCAI-2004-Harel #challenge #modelling #multi #towards

A Grand Challenge for Computing: Towards Full Reactive Modeling of a Multi-cellular Animal (DH), pp. 323–324.