Separation Logic for Verifying Physical Collisions of CNC Programs
For CNC machining safety verification, this work offers a scalable formal method that eliminates repetitive simulation tests, but it is an incremental application of existing logic to a new domain.
This paper introduces a formal verification framework for CNC machining safety that models the physical workspace as a Spatial Heap and uses Separation Logic to detect collisions as logical data races, providing a mathematically grounded alternative to simulation-based methods.
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. This approach provides a scalable, mathematically grounded alternative to geometric simulation, offering a foundation for autonomous, zero-collision manufacturing.