Kyle R. Thompson

Proof assistants enable users to develop machine-checked proofs regarding software-related properties. Unfortunately, the interactive nature of these proof assistants imposes most of the proof burden on the user, making formal verification a complex, and time-consuming endeavor. Recent automation techniques based on neural methods address this issue, but require good programmatic support for collecting data and interacting with proof assistants. This paper presents CoqPyt, a Python tool for interacting with the Coq proof assistant. CoqPyt improves on other Coq-related tools by providing novel features, such as the extraction of rich premise data. We expect our work to aid development of tools and techniques, especially LLM-based, designed for proof synthesis and repair. A video describing and demonstrating CoqPyt is available at: https://youtu.be/fk74o0rePM8.

This exploratory work investigates the feasibility of extracting linear attenuation functions with respect to energy from a multi-channel radiograph of an object of interest composed of a homogeneous material by simulating the entire imaging system combined with a digital phantom of the object of interest and leveraging this information along with the acquired multi-channel image. This synergistic combination of information allows for improved estimates on not only the attenuation for an effective energy, but for the entire spectrum of energy that is coincident with the detector elements. Material composition identification from radiographs would have wide applications in both medicine and industry. This work will focus on industrial radiography applications and will analyse a range of materials that vary in attenuative properties. This work shows that using iterative solvers holds encouraging potential to fully solve for the linear attenuation profile for the object and material of interest when the imaging system is characterized with respect to initial source x-ray energy spectrum, scan geometry, and accurate digital phantom.