Formalizing Linear Motion G-code for Invariant Checking and Differential Testing of Fabrication Tools

Watch this 15-minute conference presentation from OOPSLA 2025 that introduces a novel algorithm for formalizing G-code in computational fabrication pipelines. Learn how researchers Yumeng He, Chandrakana Nandi, and Sreepathi Pai developed GlitchFinder, a tool that lifts G-code programs to cuboid representations and creates approximate point cloud models for efficient analysis. Discover how this approach enables three key applications: error localization in CAD models through invariant checking, quantitative comparisons between different 3D slicers like Cura and PrusaSlicer, and evaluation of mesh repair tools such as MeshLab and Meshmixer. Explore the evaluation results from 58 real-world CAD models that demonstrate the tool's effectiveness in identifying slicing issues caused by small features and detecting cases where mesh repair tools introduce new errors during the repair process. Understand how this work bridges traditional compiler verification techniques with the unique challenges of 3D printing and computational fabrication, providing new methods for ensuring reliability in the fabrication pipeline from CAD design to machine code execution.