The coordination of multiple autonomous vehicles into convoys or platoons is expected on our highways in the near future. However, before such platoons can be deployed, the new autonomous behaviors of the vehicles in these platoons must be certified. An appropriate representation for vehicle platooning is as a multi-agent system in which each agent captures the "autonomous decisions" carried out by each vehicle. In order to ensure that these autonomous decision-making agents in vehicle platoons never violate safety requirements, we use formal verification. However, as the formal verification technique used to verify the agent code does not scale to the full system and as the global verification technique does not capture the essential verification of autonomous behavior, we use a combination of the two approaches. This mixed strategy allows us to verify safety requirements not only of a model of the system, but of the actual agent code used to program the autonomous vehicles.
The spread of autonomous systems into safety-critical areas has increased the demand for their formal verification, not only due to stronger certification requirements but also to public uncertainty over these new technologies. However, the complex nature of such systems, for example, the intricate combination of discrete and continuous aspects, ensures that whole system verification is often infeasible. This motivates the need for novel analysis approaches that modularise the problem, allowing us to restrict our analysis to one particular aspect of the system while abstracting away from other…
GDPR Auto-Formalization with AI Agents and Human Verification
Center for Juris-Informatics, ROIS-DS（法律信息中心，ROIS-DS）；Ruhr-University Bochum, RC-Trust（波恩鲁尔大学，RC-Trust）；Alberta Machine Intelligence Institute, University of Alberta（阿尔伯塔机器智能研究所，阿尔伯塔大学）
Agentic AI-based Coverage Closure for Formal Verification
1 Infineon Technologies India Private Limited, India 2 Dr. B R Ambedkar National Institute of Technology Jalandhar, India 3 Infineon Technologies Dresden AG \& Co. KG, Germany
Groundbreaking successes have been achieved by Deep Reinforcement Learning (DRL) in solving practical decision-making problems. Robotics, in particular, can involve high-cost hardware and human interactions. Hence, scrupulous evaluations of trained models are required to avoid unsafe behaviours in the operational environment. However, designing metrics to measure the safety of a neural network is an open problem, since standard evaluation parameters (e.g., total reward) are not informative enough. In this paper, we present a semi-formal verification approach for decision-making tasks, based on…
The theory of actual causality, defined by Halpern and Pearl, and its quantitative measure - the degree of responsibility - was shown to be extremely useful in various areas of computer science due to a good match between the results it produces and our intuition. In this paper, I describe the applications of causality to formal verification, namely, explanation of counterexamples, refinement of coverage metrics, and symbolic trajectory evaluation. I also briefly discuss recent applications of causality to legal reasoning.
IRISA（法国国家信息与自动化研究所布列塔尼大西洋分部）；University of South Brittany（南布列塔尼大学）；The Islamia University of Bahawalpur（巴哈瓦尔布尔伊斯兰大学）
It is important to have multi-agent robotic system specifications that ensure correctness properties of safety and liveness. As these systems have concurrency, and often have dynamic environment, the formal specification and verification of these systems along with step-wise refinement from abstract to concrete concepts play a major role in system correctness. Formal verification is used for exhaustive investigation of the system space thus ensuring that undetected failures in the behavior are excluded. We construct the system incrementally from subcomponents, based on software architecture. T…
MIT-IBM Watson AI Lab（MIT-IBM沃森人工智能实验室）；IBM Research（IBM研究院）；Massachusetts Institute of Technology（麻省理工学院）
Autonomous systems -- such as self-driving cars, autonomous drones, and automated trains -- must come with strong safety guarantees. Over the past decade, techniques based on formal methods have enjoyed some success in providing strong correctness guarantees for large software systems including operating system kernels, cryptographic protocols, and control software for drones. These successes suggest it might be possible to ensure the safety of autonomous systems by constructing formal, computer-checked correctness proofs. This paper identifies three assumptions underlying existing formal veri…
DafnyBench: A Benchmark for Formal Software Verification
Harvard College（哈佛学院）；Massachusetts Institute of Technology（麻省理工学院）；Northeastern University（东北大学）；Stanford University（斯坦福大学）；University of California Irvine（加州大学欧文分校）；Harvard University（哈佛大学）
ReVEAL: GNN-Guided Reverse Engineering for Formal Verification of Optimized Multipliers
University of Maryland, College Park, USA（美国马里兰大学College Park分校）；TU Wien, Austria（奥地利维也纳技术大学）；NVIDIA（英伟达公司）；Hong Kong University of Science and Technology (Guangzhou)（香港科学与技术大学（广州））
Imperial College London（帝国理工学院）；Université d’Evry（埃夫里大学）
Humans engage in informal debates on a daily basis. By expressing their opinions and ideas in an argumentative fashion, they are able to gain a deeper understanding of a given problem and in some cases, find the best possible course of actions towards resolving it. In this paper, we develop a methodology to verify debates formalised as abstract argumentation frameworks. We first present a translation from debates to transition systems. Such transition systems can model debates and represent their evolution over time using a finite set of states. We then formalise relevant debate properties usi…
Heriot-Watt University（赫瑞-瓦特大学）；University of Liverpool（利物浦大学）
The battery is a key component of autonomous robots. Its performance limits the robot's safety and reliability. Unlike liquid-fuel, a battery, as a chemical device, exhibits complicated features, including (i) capacity fade over successive recharges and (ii) increasing discharge rate as the state of charge (SOC) goes down for a given power demand. Existing formal verification studies of autonomous robots, when considering energy constraints, formalise the energy component in a generic manner such that the battery features are overlooked. In this paper, we model an unmanned aerial vehicle (UAV)…
