Ahmed Bouajjani, David Monniaux
Proceedings of the 18th International Conference on Verification, Model Checking and Abstract Interpretation
VMCAI, 2017.

@proceedings{VMCAI-2017,
	doi           = "10.1007/978-3-319-52234-0",
	editor        = "Ahmed Bouajjani and David Monniaux",
	isbn          = "978-3-319-52233-3",
	publisher     = "{Springer}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 18th International Conference on Verification, Model Checking and Abstract Interpretation}",
	volume        = 10145,
	year          = 2017,
}

Contents (29 items)

VMCAI-2017-AhmedBBDFHINPRS #ltl #model checking

Bringing LTL Model Checking to Biologists (ZA, DB, SB, ACED, JF, BAH, SI, JN, NP, MR, NS), pp. 1–13.

VMCAI-2017-CuoqRC #alias #detection #strict

Detecting Strict Aliasing Violations in the Wild (PC, LR, AC), pp. 14–33.

VMCAI-2017-AbalBW #abstraction #c #debugging #effectiveness #source code

Effective Bug Finding in C Programs with Shape and Effect Abstractions (IA, CB, AW), pp. 34–54.

VMCAI-2017-BloemCES

Synthesizing Non-Vacuous Systems (RB, HC, ME0, OS), pp. 55–72.

VMCAI-2017-BotbolCG #communication #process #static analysis #transducer #using

Static Analysis of Communicating Processes Using Symbolic Transducers (VB, EC, TLG), pp. 73–90.

VMCAI-2017-BrideKP #reduction #verification #workflow

Reduction of Workflow Nets for Generalised Soundness Verification (HB, OK, FP), pp. 91–111.

VMCAI-2017-BlazyBY #abstraction

Structuring Abstract Interpreters Through State and Value Abstractions (SB, DB, BY), pp. 112–130.

VMCAI-2017-ChakrabortyGJ #multi

Matching Multiplications in Bit-Vector Formulas (SC, AG, RJ0), pp. 131–150.

VMCAI-2017-DSilvaKS #abstraction #concurrent #independence #modelling

Independence Abstractions and Models of Concurrency (VD, DK, MS), pp. 151–168.

VMCAI-2017-DSilvaS #abstraction #logic #subclass

Complete Abstractions and Subclassical Modal Logics (VD, MS), pp. 169–186.

VMCAI-2017-FerraraT0K #abstract interpretation #fault #using

Using Abstract Interpretation to Correct Synchronization Faults (PF, OT, PL0, EK), pp. 187–208.

VMCAI-2017-FrumkinFLPSS #concurrent #fault #proving #reachability

Property Directed Reachability for Proving Absence of Concurrent Modification Errors (AF, YMYF, OL, OP, MS, SS), pp. 209–227.

VMCAI-2017-GuW #analysis #float #source code #using

Stabilizing Floating-Point Programs Using Provenance Analysis (YG, TW), pp. 228–245.

VMCAI-2017-GuntherLSW #concurrent #model checking #reduction

Dynamic Reductions for Model Checking Concurrent Software (HG, AL, AS, GW), pp. 246–265.

VMCAI-2017-HahnST0 #algorithm #game studies #recursion

Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games (EMH, SS, AT, LZ0), pp. 266–287.

VMCAI-2017-HolikHLRV #automaton #refinement #validation

Counterexample Validation and Interpolation-Based Refinement for Forest Automata (LH, MH, OL, AR, TV), pp. 288–309.

VMCAI-2017-JiangCWW #abstract domain #abstract interpretation #smt

Block-Wise Abstract Interpretation by Combining Abstract Domains with SMT (JJ, LC, XW, JW0), pp. 310–329.

VMCAI-2017-Jovanovic #integer

Solving Nonlinear Integer Arithmetic with MCSAT (DJ), pp. 330–346.

VMCAI-2017-KonnovWSS #abstraction #algorithm #distributed #fault tolerance

Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms (IVK0, JW, FS, LS), pp. 347–366.

VMCAI-2017-MarechalP #performance

Efficient Elimination of Redundancies in Polyhedra by Raytracing (AM, MP), pp. 367–385.

VMCAI-2017-MonatM #abstract interpretation #abstraction #concurrent #precise #relational #source code #thread #using

Precise Thread-Modular Abstract Interpretation of Concurrent Programs Using Relational Interference Abstractions (RM, AM), pp. 386–404.

VMCAI-2017-MukherjeeKD #detection #kernel

Detecting All High-Level Dataraces in an RTOS Kernel (SM, AK, DD), pp. 405–423.

VMCAI-2017-MuschollSW #parametricity #process #reachability

Reachability for Dynamic Parametric Processes (AM, HS, IW), pp. 424–441.

VMCAI-2017-OzeriPRS #abstract interpretation #using

Conjunctive Abstract Interpretation Using Paramodulation (OO, OP, NR, MS), pp. 442–461.

VMCAI-2017-ReynoldsIS #logic #reasoning

Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic (AR, RI, CS), pp. 462–482.

VMCAI-2017-Seladji #analysis #component

Finding Relevant Templates via the Principal Component Analysis (YS), pp. 483–499.

VMCAI-2017-SharmaR

Sound Bit-Precise Numerical Domains (TS, TWR), pp. 500–520.

VMCAI-2017-VizelGSM

IC3 - Flipping the E in ICE (YV, AG, SS, SM), pp. 521–538.

VMCAI-2017-0062BW #memory management #modelling #program analysis

Partitioned Memory Models for Program Analysis (WW0, CWB, TW), pp. 539–558.