Neil D. Jones, Markus Müller-Olm
Proceedings of the 10th International Conference on Verification, Model Checking and Abstract Interpretation
VMCAI, 2009.

@proceedings{VMCAI-2009,
	address       = "Savannah, Georgia, USA",
	doi           = "10.1007/978-3-540-93900-9",
	editor        = "Neil D. Jones and Markus Müller-Olm",
	isbn          = "978-3-540-93899-6",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 10th International Conference on Verification, Model Checking and Abstract Interpretation}",
	volume        = 5403,
	year          = 2009,
}

Contents (29 items)

6 ×#model checking
3 ×#abstraction
3 ×#source code
3 ×#using
2 ×#abstract interpretation
2 ×#analysis
2 ×#behaviour
2 ×#bound
2 ×#constraints
2 ×#probability

VMCAI-2009-Emerson #model checking #problem

Model Checking: Progress and Problems (EAE), p. 1.

VMCAI-2009-Gupta #concurrent #model checking #source code

Model Checking Concurrent Programs (AG), p. 2.

VMCAI-2009-Sagiv #analysis #thread

Thread-Modular Shape Analysis (MS), p. 3.

VMCAI-2009-Cook #liveness #roadmap #termination

Advances in Program Termination and Liveness (BC), p. 4.

VMCAI-2009-Cortier #protocol #security #verification

Verification of Security Protocols (VC), pp. 5–13.

VMCAI-2009-AmjadB #analysis #automation #proving #towards

Towards Automatic Stability Analysis for Rely-Guarantee Proofs (HA, RB), pp. 14–28.

VMCAI-2009-BentonF #behaviour #java #source code

Mostly-Functional Behavior in Java Programs (WCB, CNF), pp. 29–43.

VMCAI-2009-DimoulasW #higher-order #problem

The Higher-Order Aggregate Update Problem (CD, MW), pp. 44–58.

VMCAI-2009-EtessamiG #programming #transaction

An Abort-Aware Model of Transactional Programming (KE, PG), pp. 59–73.

VMCAI-2009-GallowayLMS #file system #linux #model checking

Model-Checking the Linux Virtual File System (AG, GL, JTM, RS), pp. 74–88.

VMCAI-2009-GodefroidP #ltl #model checking #revisited

LTL Generalized Model Checking Revisited (PG, NP), pp. 89–104.

VMCAI-2009-GondiPS #monitoring #probability

Monitoring the Full Range of omega-Regular Properties of Stochastic Systems (KG, YP, APS), pp. 105–119.

VMCAI-2009-GulwaniSV #abstraction #constraints #invariant

Constraint-Based Invariant Inference over Predicate Abstraction (SG, SS, RV), pp. 120–135.

VMCAI-2009-GurovH #behaviour #source code

Reducing Behavioural to Structural Properties of Programs with Procedures (DG, MH), pp. 136–150.

VMCAI-2009-HolzerSTV #testing

Query-Driven Program Testing (AH, CS, MT, HV), pp. 151–166.

VMCAI-2009-JurdzinskiLR #automaton #game studies #hybrid

Average-Price-per-Reward Games on Hybrid Automata with Strong Resets (MJ, RL, MR), pp. 167–181.

VMCAI-2009-KattenbeltKNP #abstraction #probability #refinement

Abstraction Refinement for Probabilistic Software (MK, MZK, GN, DP), pp. 182–197.

VMCAI-2009-KiddRDV #debugging #random #using

Finding Concurrency-Related Bugs Using Random Isolation (NK, TWR, JD, MV), pp. 198–213.

VMCAI-2009-KinderZV #abstract interpretation #control flow #framework #re-engineering

An Abstract Interpretation-Based Framework for Control Flow Reconstruction from Binaries (JK, FZ, HV), pp. 214–228.

VMCAI-2009-LavironL #approach #linear #named #scalability

SubPolyhedra: A (More) Scalable Approach to Infer Linear Inequalities (VL, FL), pp. 229–244.

VMCAI-2009-Maier

Deciding Extensions of the Theories of Vectors and Bags (PM), pp. 245–259.

VMCAI-2009-MightM #abstract interpretation #nondeterminism

A PosterioriSoundness for Non-deterministic Abstract Interpretations (MM, PM), pp. 260–274.

VMCAI-2009-Oshman #bound #model checking

An Automata-Theoretic Dynamic Completeness Criterion for Bounded Model-Checking (RO), pp. 275–289.

VMCAI-2009-RakamaricH #low level #memory management #scalability

A Scalable Memory Model for Low-Level Code (ZR, AJH), pp. 290–304.

VMCAI-2009-TalyGT #constraints #logic #theorem proving #using

Synthesizing Switching Logic Using Constraint Solving (AT, SG, AT), pp. 305–319.

VMCAI-2009-TreflerW #architecture #reduction #symmetry

Extending Symmetry Reduction by Exploiting System Architecture (RJT, TW), pp. 320–334.

VMCAI-2009-Vafeiadis #abstraction #verification

Shape-Value Abstraction for Verifying Linearizability (VV), pp. 335–348.

VMCAI-2009-WeiGC #revisited

Mixed Transition Systems Revisited (OW, AG, MC), pp. 349–365.

VMCAI-2009-WimmerBB #bound #generative #markov #model checking #using

Counterexample Generation for Discrete-Time Markov Chains Using Bounded Model Checking (RW, BB, BB), pp. 366–380.