Automated Technology for Verification and Analysis : 20th International Symposium, ATVA 2022, Virtual Event, October 25–28, 2022, Proceedings / edited by Ahmed Bouajjani, Lukáš Holík, Zhilin Wu.

Format:

Book

Contributor:

Holík, Lukás, editor.

Bouajjani, Ahmed, editor.

Wu, Zhilin, editor.

Series:

Lecture Notes in Computer Science, 1611-3349 ; 13505

Language:

English

Subjects (All):

Software engineering.

Computer engineering.

Computer networks.

Computers.

Computer science.

Artificial intelligence.

Software Engineering.

Computer Engineering and Networks.

Computer Hardware.

Theory of Computation.

Artificial Intelligence.

Local Subjects:

Software Engineering.

Computer Engineering and Networks.

Computer Hardware.

Theory of Computation.

Artificial Intelligence.

Physical Description:

1 online resource (442 pages)

Edition:

1st ed. 2022.

Place of Publication:

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

Summary:

This book constitutes the refereed proceedings of the 20th International Symposium on Automated Technology for Verification and Analysis, ATVA 2022, held in Beiging, China in October 2022. The symposium is dedicated to promoting research in theoretical and practical aspects of automated analysis, verification and synthesis by providing an international venue for the researchers to present new results. The 21 regular papers presented together with 5 tool papers and 1 invited paper were carefully reviewed and selected from 81 submissions. The papers are divided into the following topical sub-headings: reinforcement learning; program analysis and verification; smt and verification; automata and applications; active learning; probabilistic and stochastic systems; synthesis and repair; and verification of neural networks.

Contents:

Invited Paper

Learning Monitorable Operational Design Domains for Assured Autonomy

Reinforcement Learning

Dynamic Shielding for Reinforcement Learning in Black-Box Environments

An Impossibility Result in Automata-Theoretic Reinforcement Learning

Reusable Contracts for Safe Integration of Reinforcement Learning in Hybrid Systems

Program Analysis and Verification

SISL: Concolic Testing of Structured Binary Input Formats via Partial Specification

Fence Synthesis under the C11 Memory Model

Checking Scheduling-induced Violations of Control Safety Properties

Symbolic Runtime Verification for Monitoring under Uncertainties and Assumptions

SMT and Verification

Handling Polynomial and Transcendental Functions in SMT via Unconstrained Optimisation and Topological Degree Test

Verification of SMT Systems with Quantifiers

Projected Model Counting: Beyond Independent Support

Automata and Applications

Minimization of Automata for Liveness Languages

Temporal Causality in Reactive Systems

PDAAAL: A Library for Reachability Analysis of Weighted Pushdown Systems

Active Learning

Learning Deterministic One-Clock Timed Automata via Mutation Testing

Active Learning of One-Clock Timed Automata using Constraint Solving

Learning and Characterizing Fully-Ordered Lattice Automata

Probabilistic and Stochastic Systems

Optimistic and Topological Value Iteration for Simple Stochastic Games

Alternating Good-for-MDPs Automata

PET - A Partial Exploration Tool for Probabilistic Verification

STOMPC: Stochastic Model-Predictive Control with Uppaal Stratego

Synthesis and Repair

Synthesis of Parametric Hybrid Automata from Time Series

Optimal Repair For Omega-regular Properties

Repairing Real-Time Requirements

Verification of Neural Networks

An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks

Prioritizing Corners in OoD Detectors via Symbolic String Manipulation

POLAR: A Polynomial Arithmetic Framework for Verifying Neural-Network Controlled Systems.

Other Format:

Print version: Bouajjani, Ahmed Automated Technology for Verification and Analysis

ISBN:

9783031199929

3031199928