VENUS: Formal Verification for Neural Systems

Abstract

The overarching objective of the project Venus: Formal Verification of Neural Systems concerned the development of the theoretical underpinnings, methods, and tools for the formal analysis of learning-enabled cyber-physical systems (LE-CPS) and their assessment on use cases of industrial relevance within the Assured Autonomy project.Specifically the effort was aimed at:1. The formalization of the problem of formal verification for open-loop and closed-loop LE-CPS both in terms of decision problem and in terms of specifications to be verified.2. The development of algorithms and methods for the scalable verification of LE-CPS.3. The open-source development and release of a toolkit for the methods of point 2.4. The application of the tool in use cases arising from Technical Area (TA)4 performers.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jul 28, 2023
Accession Number
AD1206824

Entities

People

  • Alessio Lomuscio

Organizations

  • Imperial College London

Tags

Communities of Interest

  • Autonomy
  • Cyber
  • Energy and Power Technologies

DTIC Thesaurus Topics

  • Air Force
  • Airborne Collision Avoidance Systems
  • Artificial Intelligence
  • Artificial Intelligence Computing
  • Artificial Intelligence Software
  • Automata Theory
  • Collision Avoidance Systems
  • Computer Languages
  • Computer Programming
  • Computer Science
  • Computers
  • Control Systems
  • Detectors
  • Information Science
  • Information Systems
  • Integer Programming
  • Linear Programming
  • Machine Learning
  • Neural Networks
  • Optimization
  • Recurrent Neural Networks
  • Two Dimensional
  • Unmanned Vehicles

Fields of Study

  • Computer science

Readers

  • Agent-Based Social Robotics and Mobile-Assisted Learning in Virtual Environments.
  • Neuroscience
  • Software Engineering.

Technology Areas

  • Cyber