Proceedings of the 30st International Conference on Computer Aided Verification, Part II
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter

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

TEST
DBLP
Scholar
DOI
Full names Links ISxN
@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.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.