Computer Aided Verification: 31st International Conference, Cav 2019, New York City, Ny, Usa, July 15-18, 2019, Proceedings, Part II

ISBN-13: 9783030255428 / Angielski / Miękka / 2019 / 549 str.

Isil Dillig; Serdar Tasiran

Spis treści

Logics, Decision Procedures, and Solvers.- Satisfiability Checking for Mission-Time LTL.- High-Level Abstractions for Simplifying Extended String Constraints in SMT.- Alternating Automata Modulo First Order Theories.- Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors.- CVC4SY: Smart and Fast Term Enumeration for Syntax-Guided Synthesis.- Incremental Determinization for Quantifier Elimination and Functional Synthesis.- Numerical Programs.- Loop Summarization with Rational Vector Addition Systems.- Invertibility Conditions for Floating-Point Formulas.- Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems.- Icing: Supporting Fast-math Style Optimizations in a Verified Compiler.- Sound Approximation of Programs with Elementary Functions.- Verification.- Formal verification of quantum algorithms using quantum Hoare logic.- SecCSL: Security Concurrent Separation Logic.- Reachability Analysis for AWS-based Networks.- Distributed Systems and Networks.- Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics.- Gradual Consistency Checking.- Checking Robustness Against Snapshot Isolation.- Efficient verification of network fault tolerance via counterexampleguided refinement.- On the Complexity of Checking Consistency for Replicated Data Types.- Communication-closed asynchronous protocols.- Verification and Invariants.- Interpolating Strong Induction.- Verifying Asynchronous Event-Driven Programs Using Partial Abstract Transformers.- Inferring Inductive Invariants from Phase Structures.- Termination of Triangular Integer Loops is Decidable.- AliveInLean: A Verified LLVM Peephole Optimization Verifier.- Concurrency.- Automated Parameterized Verification of CRDTs.- What's wrong with on-the-y partial order reduction.- Integrating Formal Schedulability Analysis into a Verifed OS Kernel.- Rely-guarantee Reasoning about Concurrent Memory Management in Zephyr RTOS.- Violat: Generating Tests of Observational Refinement for Concurrent Objects.