Deepak D'Souza, Akash Lal, Kim Guldstrand Larsen
Proceedings of the 16th International Conference on Verification, Model Checking and Abstract Interpretation
VMCAI, 2015.

@proceedings{VMCAI-2015,
	address       = "Mumbai, India",
	doi           = "10.1007/978-3-662-46081-8",
	editor        = "Deepak D'Souza and Akash Lal and Kim Guldstrand Larsen",
	isbn          = "978-3-662-46080-1",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 16th International Conference on Verification, Model Checking and Abstract Interpretation}",
	volume        = 8931,
	year          = 2015,
}

Contents (25 items)

5 ×#abstraction
4 ×#verification
3 ×#analysis
3 ×#proving
2 ×#algebra
2 ×#array
2 ×#automation
2 ×#induction
2 ×#markov
2 ×#memory management

VMCAI-2015-RandourRS #probability #problem

Variations on the Stochastic Shortest Path Problem (MR, JFR, OS), pp. 1–18.

VMCAI-2015-Cousot #induction

Abstracting Induction by Extrapolation and Interpolation (PC), pp. 19–42.

VMCAI-2015-NagarS #analysis #using

Path Sensitive Cache Analysis Using Cache Miss Paths (KN, YNS), pp. 43–60.

VMCAI-2015-CortesiFPT #mobile #policy #privacy #semantics #verification

Datacentric Semantics for Verification of Privacy Policy Compliance by Mobile Applications (AC, PF, MP, OT), pp. 61–79.

VMCAI-2015-ReynoldsK #induction #smt

Induction for SMT Solvers (AR, VK), pp. 80–98.

VMCAI-2015-AdjeG #automation #invariant #linear #polynomial #source code #synthesis

Automatic Synthesis of Piecewise Linear Quadratic Invariants for Programs (AA, PLG), pp. 99–116.

VMCAI-2015-SahaEJMT #distributed #markov

Distributed Markov Chains (RS, JE, SKJ, MM, PST), pp. 117–134.

VMCAI-2015-BackesR #abstraction #analysis #clustering #graph transformation #infinity

Analysis of Infinite-State Graph Transformation Systems by Cluster Abstraction (PB, JR), pp. 135–152.

VMCAI-2015-WaezWDR #industrial #realtime

A Model for Industrial Real-Time Systems (MTBW, AW, JD, KR), pp. 153–171.

VMCAI-2015-BraitlingFHWBH #automaton #markov #metric

Abstraction-Based Computation of Reward Measures for Markov Automata (BB, LMFF, HH, RW, BB, HH), pp. 172–189.

VMCAI-2015-UrbanM #abstract interpretation #proving

Proving Guarantee and Recurrence Temporal Properties by Abstract Interpretation (CU, AM), pp. 190–208.

VMCAI-2015-KafleG #horn clause #refinement #verification

Tree Automata-Based Refinement with Application to Horn Clause Verification (BK, JPG), pp. 209–226.

VMCAI-2015-GanjeiREP #process

Abstracting and Counting Synchronizing Processes (ZG, AR, PE, ZP), pp. 227–244.

VMCAI-2015-SalaunY #algebra #debugging #process #specification

Debugging Process Algebra Specifications (GS, LY), pp. 245–262.

VMCAI-2015-BjornerG #abstraction

Property Directed Polyhedral Abstraction (NB, AG), pp. 263–281.

VMCAI-2015-LiuR #abstraction #array

Abstraction of Arrays Based on Non Contiguous Partitions (JL, XR), pp. 282–299.

VMCAI-2015-GjomemoNPVZ #optimisation #verification

From Verification to Optimizations (RG, KSN, PHP, VNV, LDZ), pp. 300–317.

VMCAI-2015-PrabhakarS #abstraction #analysis #hybrid

Foundations of Quantitative Predicate Abstraction for Stability Analysis of Hybrid Systems (PP, MGS), pp. 318–335.

VMCAI-2015-Christakis0W #evaluation

An Experimental Evaluation of Deliberate Unsoundness in a Static Program Analyzer (MC, PM, VW), pp. 336–354.

VMCAI-2015-MukundRS #bound #data type #implementation

Bounded Implementations of Replicated Data Types (MM, GSR, SPS), pp. 355–372.

VMCAI-2015-ChristakisG #composition #image #memory management #parsing #proving #safety #testing #using

Proving Memory Safety of the ANI Windows Image Parser Using Compositional Exhaustive Testing (MC, PG), pp. 373–392.

VMCAI-2015-Ferrara0N #automation

Automatic Inference of Heap Properties Exploiting Value Domains (PF, PM, MN), pp. 393–411.

VMCAI-2015-ZhuNJ #array #testing #type inference

Dependent Array Type Inference from Tests (HZ, AVN, SJ), pp. 412–430.

VMCAI-2015-GhorbalSP #algebra #difference #proving #set

A Hierarchy of Proof Rules for Checking Differential Invariance of Algebraic Sets (KG, AS, AP), pp. 431–448.

VMCAI-2015-DanMVY #abstraction #effectiveness #memory management #modelling #verification

Effective Abstractions for Verification under Relaxed Memory Models (AMD, YM, MTV, EY), pp. 449–466.