Formal Methods in Verification

Neueste Paper

• Mind the Refinement Gap: When Safe High-Level Robot Plans Produce Unsafe Executions

  Stabak Das, Priyesh Ranjan, Xiangfang Li, Lijun Qian · 5. Oktober 2026

  Language-enabled robot systems increasingly combine semantic-graph planning with temporal-logic safety monitors. We investigate a trace-completeness assumption in these systems: whether the high-level action sequence checked by a monitor represents the navigation and implicit action effects induced …

• SimuVerity: Benchmarking Agents for Engineering-Grade Simulink Model Generation

  Ruiqi Zhang, Jiahao Wang, Mingxuan Li, Haichen Luo, Chaoting Wang, Guoyu Mou, Keyu Lai, Hanchao Lv, Jiaxu Wang, Yibo Zheng, Aijun Yang, Xiaohua Wang · 5. Oktober 2026

  Existing Simulink benchmarks mainly evaluate whether generated models compile, execute, or resemble a reference model. These criteria do not establish whether a model satisfies its engineering requirements. We introduce SimuVerity, a benchmark of 101 text-to-executable Simulink model-generation task…

• Exact Distinguishability in Non-Markovian Decision Processes

  Kabir Murjani, Nisarg Patel · 2. Oktober 2026

  Non-Markovian environments are often modeled as Regular Decision Processes (RDPs), where dynamics depend on the interaction history through a finite automaton. Existing offline guarantees for RDPs rely on a distinguishability assumption on the behaviour policy but provide no means of verifying it. W…

• A Verifier Can Leak the Answer: Diagnosability Before Optimization in Closed-Loop Agent Debugging

  Peiying Zhu, Sidi Chang · 2. Oktober 2026

  Agent developers increasingly compare prompts, tools, policies, and diagnosis algorithms through simulator-grounded verifiers. A verifier can nevertheless make a solver comparison vacuous: if its probes or predicates encode the target identity, an exact optimizer may appear effective without resolvi…

• Reachability in Symmetric VASS

  {\L}ukasz Kami\'nski, S{\l}awomir Lasota · 30. September 2026

  We investigate the reachability problem in symmetric vector addition systems with states (VASS), where transitions are invariant under a group of permutations of coordinates. One extremal case, the trivial groups, yields general VASS. In another extremal case, the symmetric groups, we show that the …

• Solving Robust POMDPs with Omega-regular Objectives via Partially Observable Stochastic Games

  Durgam Latha, Dion Reji, S. Akshay, {\DJ}or{\dj}e \v{Z}ikeli\'c, Shankaranarayanan Krishna · 30. September 2026

  Robust POMDPs (RPOMDPs) generalize classical POMDPs to the setting where exact transition probabilities are not known -- rather, they are only known to belong to some uncertainty set of values. In this work, we study the problem of solving RPOMDPs with general omega-regular objectives, which subsume…

• Jaxolotl: A Unified High-Performance Benchmark Suite for LTL-Based Multi-Task RL

  Mathias Jackermeier, Jacques Cloete, Alessandro Abate · 30. September 2026

  Training agents to follow arbitrary instructions is an important goal of multi-task reinforcement learning (RL). Linear temporal logic (LTL) provides a precise and structured formalism for specifying instructions to agents, and has been successfully adopted for training generalist multi-task policie…

• Video2STL: Grounding VLM-Generated Temporal Specifications for Robot Learning

  Merve Atasever, Keyan Azbijari, Cagan Bakirci, Bo-Ruei Huang, Tolga Izdas, Zahra Shahrooei, Richard Yang, Erdem Biyik, Jyotirmoy V. Deshmukh · 30. September 2026

  Video-based policy learning is particularly promising, as it illustrates target behaviors without requiring action annotations or embodiment-matched demonstrations. A central challenge is deciding what information should be transferred from the video to the robot. Existing approaches commonly conver…

• Protected Cores Are Not Enough: Certifying AI-Proposed Revisions of Temporal Specifications

  Ruggero Lanotte · 29. September 2026

  Runtime monitoring traditionally evaluates a specification that is fixed before execution or externally modified when requirements change. In learning-enabled and data-intensive systems, however, the temporal relationships represented by a specification may themselves evolve. Allowing an AI componen…

• Progression- vs Automata-based Anticipatory Monitoring of LTL over Finite Traces (Extended Version)

  Sarah Winkler, Toryn Klassen, Sheila McIlraith, Marco Montali · 29. September 2026

  When safety-critical systems are developed from a known internal specification, their correctness can be established by model checking. In the frequent case where such a specification is unknown or inaccessible, runtime verification presents an attractive alternative, e.g., to ascertain that autonom…

• Feedback Makes Perfect: A Closed-Loop Framework for NL-to-STL Translation

  Bowen Ye, Xiang Yin · 29. September 2026

  Signal Temporal Logic (STL) enables rigorous verification and control of cyber-physical systems, but writing correct specifications requires expertise that most requirement holders lack. Large language models can translate natural-language (NL) requirements into STL, yet stronger translators alone a…

• AI Harness: Certification under Proposal-Conditioned Information for Foundation-Model Agents

  Hailin Zhong, Shengxin Zhu · 29. September 2026

  Foundation-model agents are often modeled as policies over an observed state. In deployed systems, however, a runtime may intervene only after the model has emitted a semantic proposal, making the proposal both an action candidate and a decision-time observation generated by a history-conditioned pr…

• NNV3: Expanding Neural Network Verification to New Architectures and Domains

  Anne M. Tumlin, Samuel Sasaki, Ben Wooding, Diego Manzanas Lopez, Muhammad Usama Zubair, Navid Hashemi, Hongchao Zhang, Waseem Abbas, Ipek Oguz, Meiyi Ma, Taylor T. Johnson · 25. September 2026

  We present NNV3, the latest version of the Neural Network Verification (NNV) tool, a MATLAB framework for formal verification of deep learning models and learning-enabled cyber-physical systems. Building on the set-based reachability foundation of NNV 1.0 (FFNNs, CNNs, NNCS) and NNV 2.0 (RNNs, SSNNs…

• Towards An LLM-Driven Unified Conversion Framework for BT and FSM in Autonomous Intelligent Systems

  Zhang Qi, Yang Shuo, Zhu Zhengqiu, Zhou Peng, Jiao Peng · 25. September 2026

  Finite state machine (FSM) and behavior trees (BT) are widely adopted behavioral modeling paradigms for autonomous intelligent systems. While functionally equivalent and inter-convertible in principle, existing transformation methods between FSM and BT face major challenges in preserving behavioral …

• From Reasoning Strings to Partial Orders: Verifier-Certified Rule Transport through Quotient Policy Optimization

  Bang Xie, Hao Liu, Zhiyuan Peng, Xin Yin, Chenhao Ying, Yuan Luo, Senjian Zhang, Wei Chen · 24. September 2026

  Many computations admit several valid execution orders because independent subgoals or disjoint state updates can commute. Reinforcement learning with verifiable rewards usually treats each successful trace as a separate token sequence, so serialization choices can be mistaken for logical dependenci…

• Exploring Solver-Level Warmstarting for Neural Network Verification

  Annelot Bosman, Minghao Liu, Marta Kwiatkowska, Holger Hoos, Jan van Rijn · 23. September 2026

  Neural network verification has become a key tool for providing formal guarantees on the behaviour of neural networks. However, many verification problems remain computationally intractable in the worst case: even for common adversarial robustness specifications, verification is NP-complete. Here, w…

• Compiling Sufficient Governance Context from Declared Losses and Reachable States: Exact Observation-Contract Synthesis with Cardinality and Cost Objectives

  Gaston Besanson · 23. September 2026

  We call the object this paper derives and certifies a minimal sufficient governance context: given a finite reachable-state model, a deterministic declared verdict, and candidate observable attributes, we compute sufficient observation sets, distinguish attributes that are individually indispensable…

• The Refutation Gap: Certifying Both Halves of an Optimality Claim

  Rohan Pandey · 21. September 2026

  Synthesis pipelines increasingly claim not just that a program is correct, but that it is optimal. Such a claim has two halves with radically different verification stories. The upper bound, "a program of size m exists", is witnessed by an artifact that can be re-executed, proved equivalent to its s…

• Efficient Bayes-Adaptive Reinforcement Learning with Temporal Logic Specifications

  Jonathan Hau, Alessandro Abate · 21. September 2026

  We present a novel end-to-end model-based Reinforcement Learning (RL) algorithm for efficient policy synthesis under given Linear Temporal Logic (LTL) specifications (e.g., safety or reachability) in unknown environments. To do so, a Limit-Deterministic B{\"u}chi Automaton (LDBA) representation of t…

• Large Language Models as Falsifiers for Cyber-Physical Systems

  Ali ArjomandBigdeli, Jiawei Zhou, Stanley Bak · 18. September 2026

  Falsification searches for counterexamples to formal specifications in cyber-physical systems (CPS). With specifications written in Signal Temporal Logic (STL), falsification can be formulated as a robustness optimization problem, traditionally tackled with black-box search algorithms. In parallel, …

• Real-Time Synthesis of Robust Controlled Invariant Sets for Monotone Systems

  Yasin Sonmez, Mahmoud Khaled, Majid Zamani, Murat Arcak · 15. September 2026

  Safety-critical control of autonomous systems requires formal safety certificates, such as controlled invariant sets, that must be computed online as conditions change. Although standard synthesis algorithms scale poorly with state dimension, monotone dynamical systems with lower-closed safety speci…

• The Future of Safety for SaMD

  Rhea Malhotra, Tanya Sharma, Krisha Patel, Satvika Sharma, Heena Purkait, Mehak Nehal Makhija, Aellison Cassimiro, Everett Hildenbrandt, Palina Tolmach, Jaidev Shastri · 15. September 2026

  An artificial organ carries failure consequences on the scale of an aircraft or a reactor, but the software driving it is rarely held to the same standard. Teams building them rely on testing, which only reaches the failure modes someone thought of in advance. In a pump or controller that runs insid…

• Supermartingale Certificates for Parametric MDPs

  Kaushik Mallik, {\DH}or{\dj}e \v{Z}ikeli\'c · 14. September 2026

  We consider the problems of formal verification and synthesis in parametric Markov decision processes (MDPs) with general measurable state and action spaces. The heart of our approach is a parameter flattening transformation, which allows us to transform parametric MDPs into semantically equivalent …

• Learning to adapt GR(1) specifications through degradation

  Tiberiu-Andrei Georgescu, Dalal Alrajeh, Sebastian Uchitel · 14. September 2026

  Reactive synthesis is a powerful tool for generating correct-by-construction controllers from formal specifications. GR(1) is an assume-guarantee specification framework that enables efficient synthesis, allowing synthesised controllers to be used in a wide array of applications. The limitation of s…

• Reinforcement Learning with Temporal-Logic-Based Causal Diagrams

  Yash Paliwal, Rajarshi Roy, Jean-Rapha\"el Gaglione, Nasim Baharisangari, Daniel Neider, Xiaoming Duan, Ufuk Topcu, Zhe Xu · 10. September 2026

  We study a class of reinforcement learning (RL) tasks where the objective of the agent is to accomplish temporally extended goals. In this setting, a common approach is to represent the tasks as deterministic finite automata (DFA) and integrate them into the state-space for RL algorithms. However, w…