Computer Aided Verification : 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part I / edited by Sharon Shoham, Yakir Vizel.

Format:

Book

Contributor:

Shoham, Sharon, Editor.

Vizel, Yakir, Editor.

SpringerLink (Online service)

Series:

Computer Science (SpringerNature-11645)

Lecture notes in computer science 1611-3349 ; 13371

Lecture Notes in Computer Science, 1611-3349 ; 13371

Language:

English

Subjects (All):

Software engineering.

Artificial intelligence.

Algorithms.

Computer engineering.

Computer networks.

Software Engineering.

Artificial Intelligence.

Design and Analysis of Algorithms.

Computer Engineering and Networks.

Local Subjects:

Software Engineering.

Artificial Intelligence.

Design and Analysis of Algorithms.

Computer Engineering and Networks.

Physical Description:

1 online resource (XIX, 555 pages) : 144 illustrations, 110 illustrations in color.

Edition:

1st ed. 2022.

Contained In:

Springer Nature eBook

Place of Publication:

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

System Details:

text file PDF

Summary:

This open access two-volume set LNCS 13371 and 13372 constitutes the refereed proceedings of the 34rd International Conference on Computer Aided Verification, CAV 2022, which was held in Haifa, Israel, in August 2022. The 40 full papers presented together with 9 tool papers and 2 case studies were carefully reviewed and selected from 209 submissions. The papers were organized in the following topical sections: Part I: Invited papers; formal methods for probabilistic programs; formal methods for neural networks; software Verification and model checking; hyperproperties and security; formal methods for hardware, cyber-physical, and hybrid systems. Part II: Probabilistic techniques; automata and logic; deductive verification and decision procedures; machine learning; synthesis and concurrency. This is an open access book.

Contents:

A Billion SMT Queries a Day

Program Verification with Constrained Horn Clauses

Formal Methods for Probabilistic Programs Data-Driven Invariant Learning for Probabilistic Programs

Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs

Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions

Abstraction-Renement for Hierarchical Probabilistic Models

Formal Methods for Neural Networks Shared Certificates for Neural Network Verification

Example Guided Synthesis of Linear Approximations for Neural Network Verification

Verifying Neural Networks Against Backdoor Attacks

Trainify: A CEGAR-Driven Training and Verification Framework for Safe Deep Reinforcement Learning

Neural Network Robustness as a Verication Property: A Principled Case Study

Software Verication and Model Checking The Lattice-Theoretic Essence of Property Directed Reachability Analysis

A‑ne Loop Invariant Generation via Matrix Algebra

Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes

Proof-guided Underapproximation Widening for Bounded Model Checking

SolCMC: Solidity Compiler's Model Checker

Sharygina Hyperproperties and Security Software Verication of Hyperproperties Beyond k-Safety

Abstraction Modulo Stability for Reverse Engineering

A Modular and Highly Extensible API Fuzzer for SMT Solvers

Automata and Logic FORQ-based Language Inclusion Formal Testing

Sound Automation of Magic Wands

Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition

Complementing Büchi Automata with Ranker

Deductive Verication and Decision Procedures Even Faster Conicts and Lazier Reductions for String Solvers

Local Search For SMT on Linear Integer Arithmetic

Reasoning about Data Trees using CHCs

Veried Erasure Correction in Coq with MathComp and VST

Appel End-to-end Mechanised Proof of an eBPF Virtual Machine for Microcontrollers

A DSL and Verication Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols

Machine Learning Specication-Guided Learning of Nash Equilibria with High Social Welfare

Synthesizing Fair Decision Trees via Iterative Constraint Solving

SMT-based Translation Validation for Machine Learning Compiler

Lee Verifying Fairness in Quantum Machine Learning

MoGym: Using Formal Models for Training and Verifying Decision-making Agents

Synthesis and Concurrency Synthesis and Analysis of Petri Nets from Causal Specications

Verifying generalised and structural soundness of workow nets via relaxations

Capture, Analyze, Diagnose: Realizability Checking of Requirements in FRET

Information Flow Guided Synthesis

Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation.

Other Format:

Printed edition:

ISBN:

978-3-031-13185-1

9783031131851

Access Restriction:

Restricted for use by site license.