Separation Logic for Verifying Physical Collisions of CNC Programs

• URL: http://arxiv.org/abs/2605.10437v2
• Date: Wed, 20 May 2026 01:56:18 GMT
• Title: Separation Logic for Verifying Physical Collisions of CNC Programs
• Abstract summary: Safety verification in Computer Numerical Control (CNC) has traditionally relied on repetitive tests requirements change.<n>This paper conceptualizes a formal verification framework that conceptualizes physical simulation as a Spatial, treating managed logical kinematic model.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Safety verification in Computer Numerical Control (CNC) machining has traditionally relied on simulation-based methods that require repetitive tests when requirements change. This paper introduces a formal verification framework that conceptualizes the physical CNC workspace as a Spatial Heap, treating physical occupancy as a managed logical resource. Central to our approach is a Parser-Prover Handshake that decouples machine kinematics from formal logic. By mapping tool trajectories and safety buffers into a discrete spatial model prior to evaluation, the framework enables the use of Separation Logic (SL) to verify safety via formal triples. Within this model, physical collisions are redefined as logical Spatial Data Races, detected through the failure of the separating conjunction to establish disjointness. Furthermore, we extend the methodology to collaborative environments using Concurrent Separation Logic (CSL), where physical hand-offs are verified as formal ownership transfers. Additionally, the framework scales to multi-axis kinematics (e.g., 5-axis Table-Table configurations) by treating the workpiece as a dynamically mutable spatial resource. By serving as a complement to traditional geometric simulation, this approach reduces the number of required iterative test cycles, offering a foundation for autonomous, less-collision manufacturing.

Related papers

• Semantic Drift and the Stability of Operator Control in Reasoning-Class Decision Support Systems [0.0]
  Article investigates the problem of ensuring the stability of operator control in hybrid human-machine decision support systems.<n>Latent phenomenon of semantic context drift in large language models of deep logical reasoning is verified and described.<n>Engineering recommendations are formulated for implementing dynamic relational arbitration loops.
  arXiv  Detail & Related papers  (2026-07-08T16:54:30Z)
• The Art of Interrogation: Consistency Amplifies Factuality in Spatial Reasoning [65.67266333751569]
  Current Large Reasoning Models (LRMs) exhibit remarkable general capabilities but significantly underperform in spatial reasoning tasks.<n>We propose a self-supervised reinforcement learning framework that targets the internal reasoning process without requiring ground-truth annotations.<n>We show that this label-free consistency training approaches the accuracy of models trained with ground-truth supervision and achieves similar generalization across diverse tasks and data domains.
  arXiv  Detail & Related papers  (2026-06-10T10:50:06Z)
• A Reproducible and Physically Feasible Dynamic Parameter Identification Framework for a Low-Cost Robot Arm [0.0]
  This paper presents a dynamic parameter identification framework for a low-cost robot arm driven by smart actuators.<n>Products of inertia are removed according to approximate link symmetry, reducing the rigid-body model from 65 to 39 base parameters.<n>The proposed pipeline combines preprocessing, inverse-dynamics-regressor-based ordinary least squares (OLS), conditional semidefinite-programming (SDP) projection for feasibility recovery, and closed-loop input error (CLIE) refinement.
  arXiv  Detail & Related papers  (2026-05-15T13:36:03Z)
• Correct-by-Construction G-Code Generation: A Neuro-Symbolic Approach via Separation Logic [0.0]
  This paper proposes a neuro-symbolic framework for G-code generation that seeks to integrate the neural generative capabilities of the GLLM method with formal verification via a Separation Logic prover.<n>Ultimately, this work aims to develop a self-correcting system that reduces the need for human supervision, leading to safer and verified autonomous manufacturing.
  arXiv  Detail & Related papers  (2026-05-11T13:38:51Z)
• Real-Time Projected Adaptive Control for Closed-Chain Co-Manipulative Continuum Robots [0.764671395172401]
  In co-manipulative continuum robots ( CCRs), multiple continuum arms cooperate by grasping a common flexible object.<n>In practical tasks, the flexible object's physical parameters are often unknown and vary between operations.<n>This paper presents a projected adaptive control framework for CCRs formulated at the dynamic level.
  arXiv  Detail & Related papers  (2026-04-05T22:03:23Z)
• Rethinking Scientific Modeling: Toward Physically Consistent and Simulation-Executable Programmatic Generation [8.067859101380389]
  Non-executable or physically inconsistent outputs remain prevalent under stringent engineering constraints.<n>A framework for physics-consistent automatic building modeling is proposed.<n>CivilInstruct is introduced as a domain-specific dataset that formalizes structural engineering knowledge and constraint reasoning.<n> MBEval is presented as a verification-driven benchmark that evaluates executability and structural dynamics consistency.
  arXiv  Detail & Related papers  (2026-02-06T06:57:04Z)
• Physics-informed sensor coverage through structure preserving machine learning [8.009940044669191]
  We present a machine learning framework for adaptive source localization.<n>Agents use a structure-preserving digital twin of a coupled hydrodynamic-transport system for real-time trajectory planning and data assimilation.
  arXiv  Detail & Related papers  (2025-09-12T15:54:13Z)
• AutoLayout: Closed-Loop Layout Synthesis via Slow-Fast Collaborative Reasoning [102.71841660031065]
  Auto is a fully automated method that integrates a closed-loop self-validation process within a dual-system framework.<n>The effectiveness of Auto was validated across 8 distinct scenarios, where it demonstrated a significant 10.1% improvement over SOTA methods.
  arXiv  Detail & Related papers  (2025-07-06T08:35:22Z)
• Information Science Principles of Machine Learning: A Causal Chain Meta-Framework Based on Formalized Information Mapping [7.299890614172539]
  This study addresses key challenges in machine learning, namely the absence of a unified formal theoretical framework and the lack of foundational theories for model interpretability and ethical safety.<n>We first construct a formal information model, explicitly defining the ontological states and carrier mappings of typical machine learning stages.<n>By introducing learnable and processable predicates, as well as learning and processing functions, we analyze the causal chain logic and constraint laws governing machine learning processes.
  arXiv  Detail & Related papers  (2025-05-19T14:39:41Z)
• Object-Centric Conformance Alignments with Synchronization (Extended Version) [57.76661079749309]
  We present a new formalism that combines the ability of object-centric Petri nets to capture one-to-many relations and the one of Petri nets with identifiers to compare and synchronize objects based on their identity. We propose a conformance checking approach for such nets based on an encoding in satisfiability modulo theories (SMT)
  arXiv  Detail & Related papers  (2023-12-13T21:53:32Z)
• Formal Controller Synthesis for Markov Jump Linear Systems with Uncertain Dynamics [64.72260320446158]
  We propose a method for synthesising controllers for Markov jump linear systems. Our method is based on a finite-state abstraction that captures both the discrete (mode-jumping) and continuous (stochastic linear) behaviour of the MJLS. We apply our method to multiple realistic benchmark problems, in particular, a temperature control and an aerial vehicle delivery problem.
  arXiv  Detail & Related papers  (2022-12-01T17:36:30Z)
• CoCoMoT: Conformance Checking of Multi-Perspective Processes via SMT (Extended Version) [62.96267257163426]
  We introduce the CoCoMoT (Computing Conformance Modulo Theories) framework. First, we show how SAT-based encodings studied in the pure control-flow setting can be lifted to our data-aware case. Second, we introduce a novel preprocessing technique based on a notion of property-preserving clustering.
  arXiv  Detail & Related papers  (2021-03-18T20:22:50Z)
• Risk-Averse MPC via Visual-Inertial Input and Recurrent Networks for Online Collision Avoidance [95.86944752753564]
  We propose an online path planning architecture that extends the model predictive control (MPC) formulation to consider future location uncertainties. Our algorithm combines an object detection pipeline with a recurrent neural network (RNN) which infers the covariance of state estimates. The robustness of our methods is validated on complex quadruped robot dynamics and can be generally applied to most robotic platforms.
  arXiv  Detail & Related papers  (2020-07-28T07:34:30Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.