Computer Aided Verification : 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I / 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, 11561.

Theoretical Computer Science and General Issues ; 11561

Language:

English

Subjects (All):

Software engineering.

Programming languages (Electronic computers).

Computers.

Artificial intelligence.

Computer simulation.

Computer organization.

Software Engineering.

Programming Languages, Compilers, Interpreters.

Theory of Computation.

Artificial Intelligence.

Simulation and Modeling.

Computer Systems Organization and Communication Networks.

Local Subjects:

Software Engineering.

Programming Languages, Compilers, Interpreters.

Theory of Computation.

Artificial Intelligence.

Simulation and Modeling.

Computer Systems Organization and Communication Networks.

Physical Description:

1 online resource (XIX, 673 pages) : 1003 illustrations, 106 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:

This 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:

Automata and Timed Systems

Symbolic Register Automata

Abstraction Refinement Algorithms for Timed Automata

Fast Algorithms for Handling Diagonal Constraints in Timed Automata

Safety and co-safety comparator automata for discounted-sum inclusion

Clock Bound Repair for Timed Systems

Verifying Asynchronous Interactions via Communicating Session Automata

Security and Hyperproperties

Verifying Hyperliveness

Quantitative Mitigation of Timing Side Channels

Property Directed Self Composition

Security-Aware Synthesis Using Delayed-Action Games

Automated Hypersafety Verification

Automated Synthesis of Secure Platform Mappings

Synthesis

Synthesizing Approximate Implementations for Unrealizable Specifications

Quantified Invariants via Syntax-Guided Synthesis

Efficient Synthesis with Probabilistic Constraints

Membership-based Synthesis of Linear Hybrid Automata

Overfitting in Synthesis: Theory and Practice

Proving Unrealizability for Syntax-Guided Synthesis

Model Checking

BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings

When Human Intuition Fails: Using Formal Methods to Find an Error in the "Proof" of a Multi-Agent Protocol

Extending NUXMV with Timed Transition Systems and Timed Temporal Properties

Cerberus-BMC: a Principled Reference Semantics and Exploration Tool for Concurrent and Sequential C

Cyber-physical Systems and Machine Learning

Multi-Armed Bandits for Boolean Connectives in Hybrid System Falsification

StreamLAB: Stream-based Monitoring of Cyber-Physical Systems

VerifAI: A Toolkit for the Formal Design and Analysis of Artificial Intelligence-Based Systems

The Marabou Framework for Verification and Analysis of Deep Neural Networks

Probabilistic Systems, Runtime Techniques

Probabilistic Bisimulation for Parameterized Systems

Semi-Quantitative Abstraction and Analysis of Chemical Reaction Networks

PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games

Symbolic Monitoring against Specifications Parametric in Time and Data

STAMINA: STochastic Approximate Model-checker for INfinite-state Analysis

Dynamical, Hybrid, and Reactive Systems

Local and Compositional Reasoning For Optimized Reactive Systems

Robust Controller Synthesis in Timed Büchi Automata: A Symbolic Approach

Flexible Computational Pipelines for Robust Abstraction-based Control Synthesis

Temporal Stream Logic: Synthesis beyond the Bools

Run-Time Optimization for Learned Controllers through Quantitative Games

Taming Delays in Dynamical Systems: Unbounded Verification of Delay Differential Equations.

Other Format:

Printed edition:

ISBN:

978-3-030-25540-4

9783030255404

Access Restriction:

Restricted for use by site license.