Computer Aided Verification : 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, proceedings.: 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, proceedings. Part II ([2019])

• Record Type: Book
• Other Titles: CAV 2019
• Further Information: Note: Isil Dillig, Serdar Tasiran (eds.).
• Editors: Dillig, Isil; Tasiran, Serdar
• Other Names: CAV (Conference), 31st
• Contents: 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: Gen erating Tests of Observational Refinement for Concurrent Objects.
• Publisher Details: Cham, Switzerland : SpringerOpen
• Publication Date: 2019
• Extent: 1 online resource
• Subjects: 005.1; Computer programs -- Verification -- Congresses; Software engineering; Logic design; Computer science; Computer industry; Artificial intelligence; Computer logic; Software Engineering; Logics and Meanings of Programs; Mathematical Logic and Formal Languages; System Performance and Evaluation; The Computing Profession; Logic in AI; Electronic books
• Languages: English
• ISBNs: 9783030255435; 3030255433
• Related ISBNs: 9783030255428
• Notes: Note: Description based on online resource; title from digital title page (viewed on August 23, 2019).
• Access Rights: Legal Deposit; Only available on premises controlled by the deposit library and to one user at any one time; The Legal Deposit Libraries (Non-Print Works) Regulations (UK).
• Access Usage: Restricted: Printing from this resource is governed by The Legal Deposit Libraries (Non-Print Works) Regulations (UK) and UK copyright law currently in force.