Separation Logic for Verifying Physical Collisions of CNC Programs

TL;DR

This paper presents a formal verification framework for CNC safety that models physical workspace as a Spatial Heap and uses Separation Logic to detect collisions as logical data races, reducing reliance on simulation.

Contribution

It introduces a novel formal logic-based approach to verify physical collisions in CNC machining, including multi-axis and collaborative scenarios, as an alternative to traditional simulation methods.

Findings

Framework detects collisions as logical data races.

Extends to multi-axis and collaborative CNC environments.

Reduces iterative testing in safety verification.

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.