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

ISBN-13: 9783030255398 / Angielski / Miękka / 2019 / 673 str.

Isil Dillig; Serdar Tasiran

Spis treści

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.