Isil Dillig, Serdar Tasiran
Proceedings of the 30st International Conference on Computer Aided Verification, Part II
CAV (2), 2019.

@proceedings{CAV-p2-2019,
	doi           = "10.1007/978-3-030-25543-5",
	editor        = "Isil Dillig and Serdar Tasiran",
	isbn          = "['978-3-030-25542-8', '978-3-030-25543-5']",
	publisher     = "{Springer}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 30st International Conference on Computer Aided Verification, Part II}",
	volume        = 11562,
	year          = 2019,
}

Contents (30 items)

CAV-2019-LiVR #ltl #satisfiability

Satisfiability Checking for Mission-Time LTL (JL, MYV, KYR), pp. 3–22.

CAV-2019-ReynoldsNBT #abstraction #constraints #smt #string

High-Level Abstractions for Simplifying Extended String Constraints in SMT (AR, AN, CWB, CT), pp. 23–42.

CAV-2019-IosifX #automaton #first-order

Alternating Automata Modulo First Order Theories (RI, XX), pp. 43–63.

CAV-2019-JonasS #named #performance #quantifier #smt

Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors (MJ, JS), pp. 64–73.

CAV-2019-ReynoldsBNBT #named #performance #synthesis

cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis (AR, HB, AN, CWB, CT), pp. 74–83.

CAV-2019-Rabe #functional #incremental #quantifier #synthesis

Incremental Determinization for Quantifier Elimination and Functional Synthesis (MNR), pp. 84–94.

CAV-2019-SilvermanK #summary

Loop Summarization with Rational Vector Addition Systems (JS, ZK), pp. 97–115.

CAV-2019-BrainNPRBT #float

Invertibility Conditions for Floating-Point Formulas (MB, AN, MP, AR, CWB, CT), pp. 116–136.

CAV-2019-GaoKDRSAK #induction #proving

Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems (SG, JK, JVD, NR, ASL, NA, SK), pp. 137–154.

CAV-2019-BeckerDMT #compilation #named #optimisation

Icing: Supporting Fast-Math Style Optimizations in a Verified Compiler (HB, ED, MOM, ZT), pp. 155–173.

CAV-2019-DarulovaV #approximate #source code

Sound Approximation of Programs with Elementary Functions (ED, AV), pp. 174–183.

CAV-2019-LiuZWYLLYZ #algorithm #hoare #logic #quantum #using #verification

Formal Verification of Quantum Algorithms Using Quantum Hoare Logic (JL, BZ, SW, SY, TL, YL, MY, NZ), pp. 187–207.

CAV-2019-ErnstM #concurrent #logic #named #security

SecCSL: Security Concurrent Separation Logic (GE, TM), pp. 208–230.

CAV-2019-BackesBCDGHKKKK #analysis #network #reachability

Reachability Analysis for AWS-Based Networks (JB, SB, BC, CD, AG, AJH, TK, BK, EK, JK, SM, JR0, NR, JS, MAS, PS, PS, CV, BW), pp. 231–241.

CAV-2019-BerkovitsLLPS #algorithm #composition #decidability #distributed #logic #verification

Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics (IB, ML, GL, OP, SS), pp. 245–266.

CAV-2019-ZennouBEE #consistency

Gradual Consistency Checking (RZ, AB, CE, ME), pp. 267–285.

CAV-2019-BeillahiBE #robust

Checking Robustness Against Snapshot Isolation (SMB, AB, CE), pp. 286–304.

CAV-2019-GiannarakisBMW #fault tolerance #network #performance #refinement #verification

Efficient Verification of Network Fault Tolerance via Counterexample-Guided Refinement (NG, RB, RM, DW), pp. 305–323.

CAV-2019-BiswasEE #complexity #consistency #data type #on the

On the Complexity of Checking Consistency for Replicated Data Types (RB, ME, CE), pp. 324–343.

CAV-2019-DamianDMW #protocol

Communication-Closed Asynchronous Protocols (AD, CD, AM, JW), pp. 344–363.

CAV-2019-KrishnanVGG #induction

Interpolating Strong Induction (HGVK, YV, VG, AG), pp. 367–385.

CAV-2019-LiuWL #source code #using #verification

Verifying Asynchronous Event-Driven Programs Using Partial Abstract Transformers (PL, TW, AL), pp. 386–404.

CAV-2019-FeldmanWSS #induction #invariant

Inferring Inductive Invariants from Phase Structures (YMYF, JRW, SS, MS), pp. 405–425.

CAV-2019-FrohnG #decidability #integer #termination

Termination of Triangular Integer Loops is Decidable (FF, JG), pp. 426–444.

CAV-2019-LeeHL #named #optimisation #verification

AliveInLean: A Verified LLVM Peephole Optimization Verifier (JL, CKH, NPL), pp. 445–455.

CAV-2019-NagarJ #automation #verification

Automated Parameterized Verification of CRDTs (KN, SJ), pp. 459–477.

CAV-2019-Siegel #on the fly #partial order #reduction #what

What's Wrong with On-the-Fly Partial Order Reduction (SFS), pp. 478–495.

CAV-2019-GuoLLRS #analysis #kernel #scheduling

Integrating Formal Schedulability Analysis into a Verified OS Kernel (XG, ML, ML0, LR, ZS), pp. 496–514.

CAV-2019-ZhaoS #concurrent #memory management #reasoning

Rely-Guarantee Reasoning About Concurrent Memory Management in Zephyr RTOS (YZ, DS), pp. 515–533.

CAV-2019-EmmiE #concurrent #generative #named #refinement #testing

Violat: Generating Tests of Observational Refinement for Concurrent Objects (ME, CE), pp. 534–546.