Design and implementation of a verified interpreter for additive manufacturing programs
summary
A verified interpreter for RS-274 G‑code is implemented by extracting verified components into OCaml and composing them with handwritten driver code; about 54% of the codebase is verified while 46% remains unverified (parser, I/O). Core verification uses Y3 for modal state logic and Coq plus FLock-extracted float libraries for geometry; the tool checks invariants (finite coordinates), enforces bounding‑box and arc‑bound violation detection, emits full toolpath traces, and flags failures with diagnostic reports.
AI-written summary · about
chapters (16)
- 0:00Additive manufacturing intro
- 3:05Current validation limits
- 5:33Motivation for verified verification
- 7:39RS274 G-code standard
- 13:43Verified interpreter design
- 15:48High-level interpreter design
- 18:17Verification challenges
- 20:43Y3 and Coq verification
- 23:12Physical state verification
- 24:36Effects in verified code
- 25:40Results and codebase
- 26:44Domain constraint checks
- 29:543D print tool path visualization
- 31:03Verification lessons learned
- 33:29Future directions
- 43:25Q&A
related talks
16mIntroduction to RISC-V Processor Verification
17mA reusable verification, emulation and validation flow for ASIC design
13mIntroduction to RISC-V Processor Verification
21mThe New Verification Ecosystem that Supports RISC-V Verification fo...
13mEarly RISC-V Software Verification with SIM-V
17mDemo: RISC-V Models for Verification, Software Development and Architectural Explor...
19mFormal Methods for Hardware Software Integration on RISC V Embedded Systems
30mInput-based Three-Valued Abstraction Refinement