Automated Technology for Verification and Analysis: 17th International Symposium, Atva 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings

ISBN-13: 9783030317836 / Angielski / Miękka / 2019 / 552 str.

Chen Yu-Fang; Chih-Hong Cheng; Javier Esparza

Spis treści

A Note on Game Theory and Verification.- Lazy Abstraction-Based Controller Synthesis.- Truth Assignments as Conditional Autarkies.- Can We Trust Autonomous Systems? Boundaries and Risks.- Teaching Stratego to Play Ball : Optimal Synthesis for Continuous Space MDPs.- Using Symmetry Transformations in Equivariant Dynamical Systems for their Safety Verification.- Parametric Timed Model Checking for Guaranteeing Timed Opacity.- Adaptive Online First-Order Monitoring.- Multi-Head Monitoring of Metric Temporal Logic.- An Efficient Algorithm for Computing Causal Trace Sets in Causality Checking.- Conditional Testing: O -the-Shelf Combination of Test-Case Generators.- Enhancing Symbolic Execution of Heap-based Programs with Separation Logic for Test Input Generation.- BUBEN: Automated Library Abstractions Enabling Scalable Bug Detection for Large Programs with I/O and Complex Environment.- KLUZZER: Whitebox Fuzzing on top of LLVM.- Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops.- Chain Free String Constraints.- Synthesizing Efficient Low-Precision Kernels.- New Optimizations and Heuristics for Determinization of Büchi Automata.- Approximate Automata for Omega-regular Languages.- DEQ : Equivalence Checker for Deterministic Register Automata.- LTL3TELA: Small Deterministic or Nondeterministic Automata from LTL.- Efficient Trace Encodings of Bounded Synthesis for Asynchronous Distributed Systems.- Reactive Synthesis of Graphical User Interface Glue Code.- Semantic Labelling and Learning for Parity Game Solving in LTL Synthesis.- Program Repair for Hyperproperties.- Generic Emptiness Check for Fun and Profit.- Deciding Fast Termination for Probabilistic VASS with Nondeterminism.- Are Parametric Markov Chains Monotonic.- Efficient Information-Flow Verification under Speculative Execution.- Model Checking Data Flows in Concurrent Network Updates.-Performance Evaluation of NDN Data Plane Using Statistical Model Checking.