ICFP 2024 (series) / FUNARCH 2024 (series) / FUNARCH 2024 /
Design and implementation of a verified interpreter for additive manufacturing programs
This paper describes the design of a verified tool for analyzing tool paths defined in the RS-274 language for 3d printing systems. We describe how the analyzer was designed to allow a mixture of verification and code-extraction techniques to be combined for constructing a correct toolpath analyzer written in the OCaml language. We show how we moved from a fully hand-written OCaml program to one incorporating verified components, highlighting architectural decisions that were made to facilitate this process. Finally, we share a set of architectural lessons that are generally applicable to other software with a similar goal of integration of verified components.
Fri 6 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Fri 6 Sep
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
11:00 - 12:30 | |||
11:00 45mResearch paper | F3: A Compiler For Feature Engineering FUNARCH Weixi Ma Meta, Arnaud Venet Facebook, Junhua Gu Meta, Subbu Subramanian Meta, Siyu Wang Meta, Rocky Liu Meta, Daniel Friedman Indiana University, Yafei Yang | ||
11:45 45mExperience report | Design and implementation of a verified interpreter for additive manufacturing programs FUNARCH Matthew Sottle Lawrence Livermore National Laboratory, Mohit Tekriwal Lawrence Livermore National Laboratory |