Formal Methods in Verification

Últimos artículos

• Reachability in Symmetric VASS

  {\L}ukasz Kami\'nski, S{\l}awomir Lasota · 30 de septiembre de 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 de septiembre de 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 de septiembre de 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 de septiembre de 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 de septiembre de 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 de septiembre de 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 de septiembre de 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 de septiembre de 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 de septiembre de 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 de septiembre de 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 de septiembre de 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 de septiembre de 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 de septiembre de 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 de septiembre de 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 de septiembre de 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 de septiembre de 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 de septiembre de 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 de septiembre de 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 de septiembre de 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 de septiembre de 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 de septiembre de 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…

• No Free Checker: A Survey of Verifiers for Robot Policies

  Yang Wan, Xihang Yue, Zhirui Liu, Ziyuan Chu, Shuxun Wang, Yuhan Chen, Xiaonan Jiang, Xukun Zhu, Yubo Dong, Linchao Zhu · 10 de septiembre de 2026

  A verifier for robot policies reads a candidate behavior and returns a score for how well it did, used both to evaluate vision-language-action policies and to train them. Verifiers range from success detectors and reward models to runtime monitors, safety filters, and temporal-logic specifications. …

• Application of curiosity driven exploration methods for hardware interference identification

  Ludovic Matar, Clement Moulin-Frier, Pierre-Yves Oudeyer · 9 de septiembre de 2026

  The transition from single-core to multi-core architectures in safety-critical embedded systems introduces significant challenges due to inter-core interference caused by contention for shared hardware resources. Such interference affects execution times and complicates the verification of strict te…

• Generator-Independent Runtime Assurance under Partial Observation

  Guangxi Wan, Yongbo Xie, Yuqi Liu, Qingwei Dong, Qingxin Li, Hongfei Bai, Peng Zeng · 9 de septiembre de 2026

  Proposal-based controllers---learned policies, language-model planners, and other black-box \emph{generators}---are increasingly deployed behind runtime verification gates. We ask when the closed-loop safety guarantee decouples from the generator. The prevailing per-candidate certification pattern d…

• SiLR: Structure-Preserving Admission and Process Reward for LLM Tool Agents

  Chenyu Zhou, Qiliang Jiang, Shuning Wu, Xu Zhou · 7 de septiembre de 2026

  A runtime gate for an LLM tool agent is usually cast as a filter. In a ReAct loop a rejected proposal is followed by another at the same state, so the gate is a search operator over the proposal stream whose admission criterion shapes which trajectories are reachable. We study post-violation recover…