Kenneth L. McMillan, Xavier Rival
Proceedings of the 15th International Conference on Verification, Model Checking and Abstract Interpretation
VMCAI, 2014.

@proceedings{VMCAI-2014,
	address       = "San Diego, California, USA",
	doi           = "10.1007/978-3-642-54013-4",
	editor        = "Kenneth L. McMillan and Xavier Rival",
	isbn          = "978-3-642-54012-7",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 15th International Conference on Verification, Model Checking and Abstract Interpretation}",
	volume        = 8318,
	year          = 2014,
}

Contents (26 items)

5 ×#analysis
5 ×#synthesis
4 ×#source code
3 ×#safety
3 ×#verification
2 ×#abstract interpretation
2 ×#algorithm
2 ×#integer
2 ×#logic
2 ×#modelling

VMCAI-2014-BloemKS #safety #satisfiability #specification #synthesis

SAT-Based Synthesis Methods for Safety Specs (RB, RK, MS), pp. 1–20.

VMCAI-2014-SchwarzSVA #analysis #precise #source code

Precise Analysis of Value-Dependent Synchronization in Priority Scheduled Programs (MDS, HS, VV, KA), pp. 21–38.

VMCAI-2014-Mine #abstract interpretation #analysis #relational #thread

Relational Thread-Modular Static Value Analysis by Abstract Interpretation (AM), pp. 39–58.

VMCAI-2014-GustavssonGL #analysis #execution #parallel #using

Timing Analysis of Parallel Software Using Abstract Execution (AG, JG, BL), pp. 59–77.

VMCAI-2014-Chatterjee0FR #game studies

Doomsday Equilibria for Omega-Regular Games (KC, LD, EF, JFR), pp. 78–97.

VMCAI-2014-Song0G #bisimulation #logic #markov #process

Bisimulations and Logical Characterizations on Continuous-Time Markov Decision Processes (LS, LZ, JCG), pp. 98–117.

VMCAI-2014-KiniV #automaton #ltl #probability #safety #specification

Probabilistic Automata for Safety LTL Specifications (DK, MV), pp. 118–136.

VMCAI-2014-Chang #reachability

Refuting Heap Reachability (BYEC), pp. 137–141.

VMCAI-2014-WangBW

Cascade 2.0 (WW, CB, TW), pp. 142–160.

VMCAI-2014-DragoiHVWZ #algorithm #framework #verification

A Logic-Based Framework for Verifying Consensus Algorithms (CD, TAH, HV, JW, DZ), pp. 161–181.

VMCAI-2014-AngelisFPP #array #source code #verification

Verifying Array Programs by Transforming Verification Conditions (EDA, FF, AP, MP), pp. 182–202.

VMCAI-2014-LopesM #compilation #optimisation #synthesis

Weakest Precondition Synthesis for Compiler Optimizations (NPL, JM), pp. 203–221.

VMCAI-2014-JezequelE #algorithm #distributed #message passing #protocol #verification

Message-Passing Algorithms for the Verification of Distributed Protocols (LJ, JE), pp. 222–241.

VMCAI-2014-BozgaIK #integer #problem #safety #source code

Safety Problems Are NP-complete for Flat Integer Programs with Octagonal Loops (MB, RI, FK), pp. 242–261.

VMCAI-2014-AminofJKR #model checking

Parameterized Model Checking of Token-Passing Systems (BA, SJ, AK, SR), pp. 262–281.

VMCAI-2014-Fu #abstract domain #analysis #java #points-to #scalability

Modularly Combining Numeric Abstract Domains with Points-to Analysis, and a Scalable Static Numeric Analyzer for Java (ZF), pp. 282–301.

VMCAI-2014-Ferrara #abstract interpretation #analysis

Generic Combination of Heap and Value Analyses in Abstract Interpretation (PF), pp. 302–321.

VMCAI-2014-AcunaAMS #approach #complexity #heuristic #modelling #network

Modeling Parsimonious Putative Regulatory Networks: Complexity and Heuristic Approach (VA, AA, AM, AS), pp. 322–336.

VMCAI-2014-Romano #float #integer #testing

Practical Floating-Point Tests with Integer Code (AR), pp. 337–356.

VMCAI-2014-FaymonvilleFP #logic #monitoring #parametricity

Monitoring Parametric Temporal Logic (PF, BF, DP), pp. 357–375.

VMCAI-2014-WangH #concurrent #reachability

Precisely Deciding Control State Reachability in Concurrent Traces with Limited Observability (CW, KH), pp. 376–394.

VMCAI-2014-SinghSXKS #composition #modelling #sketching #synthesis #using

Modular Synthesis of Sketches Using Models (RS, RS, ZX, RK, ASL), pp. 395–414.

VMCAI-2014-EhlersSK #identifier #synthesis

Synthesis with Identifiers (RE, SAS, HKG), pp. 415–433.

VMCAI-2014-LeikeT #polynomial #source code #synthesis

Synthesis for Polynomial Lasso Programs (JL, AT), pp. 434–452.

VMCAI-2014-Masse #policy #ranking #termination

Policy Iteration-Based Conditional Termination and Ranking Functions (DM), pp. 453–471.

VMCAI-2014-HardekopfWCK #control flow

Widening for Control-Flow (BH, BW, BRC, VK), pp. 472–491.