Rupak Majumdar, Viktor Kuncak
Proceedings of the 28th International Conference on Computer Aided Verification, Part II
CAV (2), 2017.

@proceedings{CAV-p2-2017,
	doi           = "10.1007/978-3-319-63390-9",
	editor        = "Rupak Majumdar and Viktor Kuncak",
	isbn          = "['978-3-319-63389-3', '978-3-319-63390-9']",
	publisher     = "{Springer}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 28th International Conference on Computer Aided Verification, Part II}",
	volume        = 10427,
	year          = 2017,
}

Contents (32 items)

CAV-2017-AmyRS #compilation

Verified Compilation of Space-Efficient Reversible Circuits (MA, MR, KMS), pp. 3–21.

CAV-2017-TouzeauMMR #analysis #nondeterminism #performance

Ascertaining Uncertainty for Efficient Exact Cache Analysis (VT, CM, DM, JR), pp. 22–40.

CAV-2017-ChatterjeeFG #analysis #recursion #source code #worst-case

Non-polynomial Worst-Case Analysis of Recursive Programs (KC, HF0, AKG), pp. 41–63.

CAV-2017-Carbonneaux0RS #analysis #automation #coq #proving

Automated Resource Analysis with Coq Proof Objects (QC, JH0, TWR, ZS), pp. 64–85.

CAV-2017-GasconTCM #component #proving #synthesis

Look for the Proof to Find the Program: Decorated-Component-Based Program Synthesis (AG, AT0, BC, UM), pp. 86–103.

CAV-2017-SinghBM #debugging #detection #fault #formal method #locality #named #validation

E-QED: Electrical Bug Localization During Post-silicon Validation Enabled by Quick Error Detection and Formal Methods (ES, CWB, SM), pp. 104–125.

CAV-2017-EkiciMTKKRB #coq #named #plugin #smt

SMTCoq: A Plug-In for Integrating SMT Solvers into Coq (BE, AM, CT, CK, GK, AR, CWB), pp. 126–133.

CAV-2017-Fearnley #game studies #parallel #performance

Efficient Parallel Strategy Improvement for Parity Games (JF), pp. 137–154.

CAV-2017-FortinMW #automaton #linear #model checking

Model-Checking Linear-Time Properties of Parametrized Asynchronous Shared-Memory Pushdown Systems (MF, AM, IW), pp. 155–175.

CAV-2017-SaarikiviV #transducer

Minimization of Symbolic Transducers (OS, MV), pp. 176–196.

CAV-2017-SousaRDK #abstract interpretation

Abstract Interpretation with Unfoldings (MS, CR, VD, DK), pp. 197–216.

CAV-2017-MaricSB #algorithm #bound

Cutoff Bounds for Consensus Algorithms (OM, CS0, DAB), pp. 217–237.

CAV-2017-BeameL #integer #towards #verification

Towards Verifying Nonlinear Integer Arithmetic (PB, VL), pp. 238–258.

CAV-2017-El-HassanyTVV #synthesis

Network-Wide Configuration Synthesis (AEH, PT, LV, MTV), pp. 261–281.

CAV-2017-GrossmanCIRS #equivalence #source code #verification

Verifying Equivalence of Spark Programs (SG, SC, SI, NR, MS), pp. 282–300.

CAV-2017-McClurgHC #network #source code #synthesis

Synchronization Synthesis for Network Programs (JM, HH, PC), pp. 301–321.

CAV-2017-FaymonvilleFT #bound #framework #named #synthesis

BoSy: An Experimentation Framework for Bounded Synthesis (PF, BF, LT), pp. 325–332.

CAV-2017-KhalimovB #bound #synthesis

Bounded Synthesis for Streett, Rabin, and CTL* (AK, RB), pp. 333–352.

CAV-2017-AlmagorKRV #synthesis

Quantitative Assume Guarantee Synthesis (SA, OK, JOR, YV), pp. 353–374.

CAV-2017-CardelliCFKLPW #network #synthesis

Syntax-Guided Optimal Synthesis for Chemical Reaction Networks (LC, MC0, MF, MZK, LL, NP, MW), pp. 375–395.

CAV-2017-TrinhCJ #recursion #string

Model Counting for Recursively-Defined Strings (MTT, DHC, JJ), pp. 399–418.

CAV-2017-ConchonIJMF #float #reasoning #smt

A Three-Tier Strategy for Reasoning About Floating-Point Numbers in SMT (SC, MI, KJ, GM, CF), pp. 419–435.

CAV-2017-Nadel

A Correct-by-Decision Solution for Simultaneous Place and Route (AN), pp. 436–452.

CAV-2017-ReynoldsWBBLT #scalability #string #using

Scaling Up DPLL(T) String Solvers Using Context-Dependent Simplification (AR, MW, CWB, DB, TL, CT), pp. 453–474.

CAV-2017-Tentrup #on the

On Expansion and Resolution in CEGAR Based QBF Solving (LT), pp. 475–494.

CAV-2017-LeT0C #decidability #induction #logic

A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic (QLL, MT, JS0, WNC), pp. 495–517.

CAV-2017-DanS0JV #analysis

Finding Fix Locations for CFL-Reachability Analyses via Minimum Cuts (AMD, MS, SC0, JBJ, MTV), pp. 521–541.

CAV-2017-BouajjaniEEM #proving #simulation #using

Proving Linearizability Using Forward Simulations (AB, ME, CE, SOM), pp. 542–563.

CAV-2017-FinkbeinerHS #equivalence #named #satisfiability

EAHyper: Satisfiability, Implication, and Equivalence Checking of Hyperproperties (BF, CH, MS), pp. 564–570.

CAV-2017-UnnoTS #automation #horn clause #induction

Automating Induction for Solving Horn Clauses (HU0, ST, HS), pp. 571–591.

CAV-2017-DehnertJK0 #model checking #probability

A Storm is Coming: A Modern Probabilistic Model Checker (CD, SJ, JPK, MV0), pp. 592–600.

CAV-2017-Ben-AmramG #multi #on the #ranking

On Multiphase-Linear Ranking Functions (AMBA, SG), pp. 601–620.