Computer Aided Verification : 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II / edited by Isil Dillig, Serdar Tasiran.

Format:

Book

Contributor:

Dillig, Isil, editor.

Tasiran, Serdar, editor.

SpringerLink (Online service)

Series:

Computer Science (Springer-11645)

LNCS sublibrary. Theoretical computer science and general issues ; SL 1, 11562.

Theoretical Computer Science and General Issues ; 11562

Language:

English

Subjects (All):

Software engineering.

Computer logic.

Logic, Symbolic and mathematical.

Computer system failures.

Computers.

Artificial intelligence.

Software Engineering.

Logics and Meanings of Programs.

Mathematical Logic and Formal Languages.

System Performance and Evaluation.

The Computing Profession.

Logic in AI.

Local Subjects:

Software Engineering.

Logics and Meanings of Programs.

Mathematical Logic and Formal Languages.

System Performance and Evaluation.

The Computing Profession.

Logic in AI.

Physical Description:

1 online resource (XX, 549 pages) : 1209 illustrations, 42 illustrations in color.

Edition:

First edition 2019.

Contained In:

Springer eBooks

Place of Publication:

Cham : Springer International Publishing : Imprint: Springer, 2019.

System Details:

text file PDF

Summary:

The open access two-volume set LNCS 11561 and 11562 constitutes the refereed proceedings of the 31st International Conference on Computer Aided Verification, CAV 2019, held in New York City, USA, in July 2019. The 52 full papers presented together with 13 tool papers and 2 case studies, were carefully reviewed and selected from 258 submissions. The papers were organized in the following topical sections: Part I: automata and timed systems; security and hyperproperties; synthesis; model checking; cyber-physical systems and machine learning; probabilistic systems, runtime techniques; dynamical, hybrid, and reactive systems; Part II: logics, decision procedures; and solvers; numerical programs; verification; distributed systems and networks; verification and invariants; and concurrency. .

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: Generating Tests of Observational Refinement for Concurrent Objects. .

Other Format:

Printed edition:

ISBN:

978-3-030-25543-5

9783030255435

Access Restriction:

Restricted for use by site license.