Constantin Enea, Ruzica Piskac
Proceedings of the 20th International Conference on Verification, Model Checking and Abstract Interpretation
VMCAI, 2019.

@proceedings{VMCAI-2019,
	doi           = "10.1007/978-3-030-11245-5",
	editor        = "Constantin Enea and Ruzica Piskac",
	isbn          = "['978-3-030-11244-8', '978-3-030-11245-5']",
	publisher     = "{Springer}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 20th International Conference on Verification, Model Checking and Abstract Interpretation}",
	volume        = 11388,
	year          = 2019,
}

Contents (27 items)

VMCAI-2019-RaadLV #on the #semantics

On the Semantics of Snapshot Isolation (AR, OL, VV), pp. 1–23.

VMCAI-2019-SmithA #equivalence #reduction #synthesis

Program Synthesis with Equivalence Reduction (CS, AA), pp. 24–47.

VMCAI-2019-HamzaK #string #synthesis

Minimal Synthesis of String to String Functions from Examples (JH, VK), pp. 48–69.

VMCAI-2019-NguyenTC #automation #program repair #using #verification

Automatic Program Repair Using Formal Verification and Expression Templates (TTN, QTT, WNC), pp. 70–91.

VMCAI-2019-FedyukovichGG #effectiveness #functional #lazy evaluation #synthesis

Lazy but Effective Functional Synthesis (GF, AG, AG), pp. 92–113.

VMCAI-2019-BallabrigaFGLR #memory management #static analysis #using

Static Analysis of Binary Code with Memory Indirections Using Polyhedra (CB, JF, LG, GL, JR), pp. 114–135.

VMCAI-2019-BoutonnetH #abstract interpretation #interprocedural #program analysis #relational

Disjunctive Relational Abstract Interpretation for Interprocedural Program Analysis (RB, NH), pp. 136–159.

VMCAI-2019-BouillaguetBSY #analysis #deduction #in memory #memory management #modelling #pointer #verification

Exploiting Pointer Analysis in Memory Models for Deductive Verification (QB, FB, MS, BY), pp. 160–182.

VMCAI-2019-KarlSBM #fault #robust #source code #verification

Small Faults Grow Up - Verification of Error Masking Robustness in Arithmetically Encoded Programs (AFK, RS, RB, SM), pp. 183–204.

VMCAI-2019-GermaneM #analysis #automaton #continuation

Relatively Complete Pushdown Analysis of Escape Continuations (KG, MM), pp. 205–225.

VMCAI-2019-GermaneM0M #analysis #control flow

Demand Control-Flow Analysis (KG, JM, MDA0, MM), pp. 226–246.

VMCAI-2019-NicolaySMR #analysis

Effect-Driven Flow Analysis (JN, QS, WDM, CDR), pp. 247–274.

VMCAI-2019-LuCC0 #bound #source code

Type-Directed Bounding of Collections in Reactive Programs (TL, PC, BYEC, AT0), pp. 275–296.

VMCAI-2019-HoenickeS #array #constant

Solving and Interpolating Constant Arrays Based on Weak Equivalences (JH, TS), pp. 297–317.

VMCAI-2019-QiuW #decidability #logic #metric

A Decidable Logic for Tree Data-Structures with Measurements (XQ, YW), pp. 318–341.

VMCAI-2019-MurphyK #algorithm

A Practical Algorithm for Structure Embedding (CM, ZK), pp. 342–362.

VMCAI-2019-BuenoS #model checking #named

euforia: Complete Software Model Checking with Uninterpreted Functions (DB, KAS), pp. 363–385.

VMCAI-2019-LopesR #performance #scalability #simulation

Fast BGP Simulation of Large Datacenters (NPL, AR), pp. 386–408.

VMCAI-2019-AndreFMS #abstraction #algorithm #industrial #model checking #parametricity #using #verification

Verification of an Industrial Asynchronous Leader Election Algorithm Using Abstractions and Parametric Model Checking (ÉA, LF, JMM, RS), pp. 409–424.

VMCAI-2019-YamaguchiBRIK #abstract interpretation

Application of Abstract Interpretation to the Automotive Electronic Control System (TY, MB, CR, YI, YK), pp. 425–445.

VMCAI-2019-FoxSH #partial order #probability #reachability

Syntactic Partial Order Compression for Probabilistic Reachability (GF, DS, HH), pp. 446–467.

VMCAI-2019-FuC #nondeterminism #probability #source code #termination

Termination of Nondeterministic Probabilistic Programs (HF0, KC), pp. 468–490.

VMCAI-2019-AndreDFL #parametricity #protocol

Parametric Timed Broadcast Protocols (ÉA, BD, PF, DL), pp. 491–512.

VMCAI-2019-DeckerP #ltl #model checking #quantifier #using

Flat Model Checking for Counting LTL Using Quantifier-Free Presburger Arithmetic (ND, AP), pp. 513–534.

VMCAI-2019-HuybersL #algorithm #bisimulation #parallel

A Parallel Relation-Based Algorithm for Symbolic Bisimulation Minimization (RH, AL), pp. 535–554.

VMCAI-2019-HaarKP #modelling #parametricity #reduction #refinement

Combining Refinement of Parametric Models with Goal-Oriented Reduction of Dynamics (SH, JK, LP), pp. 555–576.

VMCAI-2019-PreoteasaDT #diagrams #proving

Mechanically Proving Determinacy of Hierarchical Block Diagram Translations (VP, ID, ST), pp. 577–600.