Rupak Majumdar, Viktor Kuncak
Proceedings of the 29th International Conference on Computer Aided Verification, Part I
CAV (1), 2017.

@proceedings{CAV-p1-2017,
	doi           = "10.1007/978-3-319-63387-9",
	editor        = "Rupak Majumdar and Viktor Kuncak",
	isbn          = "['978-3-319-63386-2', '978-3-319-63387-9']",
	publisher     = "{Springer}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 29th International Conference on Computer Aided Verification, Part I}",
	volume        = 10426,
	year          = 2017,
}

Contents (29 items)

CAV-2017-HuangKWW #network #safety #verification

Safety Verification of Deep Neural Networks (XH0, MK, SW, MW), pp. 3–29.

CAV-2017-Vafeiadis #consistency #logic #memory management #using #verification

Program Verification Under Weak Memory Consistency Using Separation Logic (VV), pp. 30–46.

CAV-2017-DAntoniV #automaton #power of #transducer

The Power of Symbolic Automata and Transducers (LD, MV), pp. 47–67.

CAV-2017-SiZGN #analysis #satisfiability

Maximum Satisfiability in Software Analysis: Applications and Techniques (XS, XZ, RG, MN), pp. 68–94.

CAV-2017-KatzBDJK #named #network #performance #smt #verification

Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks (GK, CWB, DLD, KJ, MJK), pp. 97–117.

CAV-2017-ChatterjeeFM #analysis #automation #bound

Automated Recurrence Analysis for Almost-Linear Expected-Runtime Bounds (KC, HF0, AM), pp. 118–139.

CAV-2017-QuatmannJK #automaton #markov #multi

Markov Automata with Multiple Objectives (TQ, SJ, JPK), pp. 140–159.

CAV-2017-Baier0L0W #markov #model checking #process #reliability

Ensuring the Reliability of Your Model Checker: Interval Iteration for Markov Decision Processes (CB, JK0, LL, DP0, SW), pp. 160–180.

CAV-2017-AlbarghouthiDD #nondeterminism #source code

Repairing Decision-Making Programs Under Uncertainty (AA, LD, SD), pp. 181–200.

CAV-2017-AshokCDKM #markov #process

Value Iteration for Long-Run Average Reward in Markov Decision Processes (PA, KC, PD, JK, TM), pp. 201–221.

CAV-2017-RoehmHM #named #validation

STLInspector: STL Validation with Guarantees (HR, TH0, ECM), pp. 225–232.

CAV-2017-BielikRV #learning

Learning a Static Analyzer from Data (PB, VR, MTV), pp. 233–253.

CAV-2017-Drachsler-Cohen #synthesis

Synthesis with Abstract Examples (DDC, SS, EY), pp. 254–278.

CAV-2017-ChasinsP #data-driven #probability #source code #synthesis

Data-Driven Synthesis of Full Probabilistic Programs (SC, PMP), pp. 279–304.

CAV-2017-Vazquez-Chanlatte #clustering #learning #logic

Logical Clustering and Learning for Time-Series Data (MVC, JVD, XJ, SAS), pp. 305–325.

CAV-2017-Ulus #monitoring #named #regular expression

Montre: A Tool for Monitoring Timed Regular Expressions (DU), pp. 329–335.

CAV-2017-SelyuninJNRHBNG #communication #monitoring #protocol #runtime

Runtime Monitoring with Recovery of the SENT Communication Protocol (KS, SJ, TN, CR, UH, EB, DN, RG), pp. 336–355.

CAV-2017-BasinKZ #data type #runtime #verification

Runtime Verification of Temporal Properties over Out-of-Order Data Streams (DAB, FK, EZ), pp. 356–376.

CAV-2017-CyrankaIBJSG

Lagrangian Reachabililty (JC, MAI, GB, PLJ, SAS, RG), pp. 379–400.

CAV-2017-BakD #linear #reachability #scalability

Simulation-Equivalent Reachability of Large Linear Systems with Inputs (SB, PSD), pp. 401–420.

CAV-2017-BrihayeGHM #automaton #composition #named

MightyL: A Compositional Translation from MITL to Timed Automata (TB, GG, HMH, BM), pp. 421–440.

CAV-2017-FanQM0 #composition #data-driven #named #reasoning #verification

DryVR: Data-Driven Verification and Compositional Reasoning for Automotive Systems (CF, BQ, SM, MV0), pp. 441–461.

CAV-2017-AbateBCCDKKP #automation #physics #synthesis

Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants (AA, IB, DC, LCC, CD, PK, DK, EP), pp. 462–482.

CAV-2017-AdimoolamDDKJ #classification #embedded

Classification and Coverage-Based Falsification for Embedded Control Systems (ASA, TD, AD, JK, XJ), pp. 483–503.

CAV-2017-AlurDLS #detection #gpu #named #source code

GPUDrano: Detecting Uncoalesced Accesses in GPU Programs (RA, JD, OSNL, NS), pp. 507–525.

CAV-2017-AlbertABGS #partial order #reduction

Context-Sensitive Dynamic Partial Order Reduction (EA, PA, MGdlB, MGZ, PJS), pp. 526–543.

CAV-2017-WindsorDSP #concurrent #lightweight #named #verification

Starling: Lightweight Concurrency Verification with Views (MW, MD, BS, MJP), pp. 544–569.

CAV-2017-WijsN #composition #incremental #model checking

Compositional Model Checking with Incremental Counter-Example Construction (AW, TN), pp. 570–590.

CAV-2017-BenesBDPS #named #parallel #parametricity #synthesis

Pithya: A Parallel Tool for Parameter Synthesis of Piecewise Multi-affine Dynamical Systems (NB, LB, MD, SP, DS), pp. 591–598.