Trigger for Momentum Calibration and Beam Position Monitoring by Means of Decay-in-Orbit $\mu$ in the Mu2e Experiment [Poster]
A poster describing the experiment is provided.
46 INSTRUMENTATION RELATED TO NUCLEAR SCIENCE AND ↗
Engineering topics
Whalen, Michael
Publications and source records attributed to Whalen, Michael.
Calibration Trigger and Beam Monitoring for the Mu2e Experiment by Means of Decay-in-Orbit $\mu$
Over the last few decades, more evidence has come out to suggest that lepton flavor may not be conserved, making the study of charged lepton flavor violation all the more important. A promising way to observe this phenomenon is through muon conversion to electron (in the case without neutrinos produced) on Al, as will occur in the Mu2e experiment, which will run over the course of three years, beginning in 2023. A major part of the apparatus is the aluminum muon stopping target, which a beam of muons hits before releasing the products of muon interactions into the tracker and calorimeter. A muon stopped in the stopping target can undergo three different processes: nuclear capture, decay in orbit and electron conversion, the last of which makes up the E=105 MeV signal we are aiming to observe. Many muons, however, are scattered into a proton absorber around this target. Muons scattered in this way eventually get stopped in the absorber and then undergo decay-in-orbit , with ele ctron products that peak in their momentum distribution at about 50 MeV/c, giving a reference peak that can be used to calibrate the tracker momentum response. A track trigger was then developed to select events with these tracks. The muon beam used in the Mu2e experiment, however, due to the magnetic field on the beam line, is tilted slightly downward, such that more particles interact with the lower part of the tracker. For calibration purposes it is preferable to have a homogeneous distribution of electrons in the tracker volume, requiring a pre-scale factor that is dependent upon the azimuthal angle of the trajectory of closest approach of the helix to the solenoidal axis (“phi”). The factor in question was then found by running Monte Carlo simulations of the electrons produced in the muon decay in the proton absorber, overlaid with background particles. In addition to being used as means to calibrate momentum distribution, these electron tracks can be used to monitor the muon beam profile for changes over time.Here, these processes are explained in greater detail, and the result of the expected trigger performance is presented.
72 PHYSICS OF ELEMENTARY PARTICLES AND FIELDS↗
Synthesizing Certified Code
Code certification is a lightweight approach to demonstrate software quality on a formal level. Its basic idea is to require producers to provide formal proofs that their code satisfies certain quality properties. These proofs serve as certificates which can be checked independently. Since code certification uses the same underlying technology as program verification, it also requires many detailed annotations (e.g., loop invariants) to make the proofs possible. However, manually adding theses annotations to the code is time-consuming and error-prone. We address this problem by combining code certification with automatic program synthesis. We propose an approach to generate simultaneously, from a high-level specification, code and all annotations required to certify generated code. Here, we describe a certification extension of AUTOBAYES, a synthesis tool which automatically generates complex data analysis programs from compact specifications. AUTOBAYES contains sufficient high-level domain knowledge to generate detailed annotations. This allows us to use a general-purpose verification condition generator to produce a set of proof obligations in first-order logic. The obligations are then discharged using the automated theorem E-SETHEO. We demonstrate our approach by certifying operator safety for a generated iterative data classification program without manual annotation of the code.
Whalen, Michael↗
AutoBayes/CC: Combining Program Synthesis with Automatic Code Certification: System Description
Code certification is a lightweight approach to formally demonstrate software quality. It concentrates on aspects of software quality that can be defined and formalized via properties, e.g., operator safety or memory safety. Its basic idea is to require code producers to provide formal proofs that their code satisfies these quality properties. The proofs serve as certificates which can be checked independently, by the code consumer or by certification authorities, e.g., the FAA. It is the idea underlying such approaches as proof-carrying code [6]. Code certification can be viewed as a more practical version of traditional Hoare-style program verification. The properties to be verified are fairly simple and regular so that it is often possible to use an automated theorem prover to automatically discharge all emerging proof obligations. Usually, however, the programmer must still splice auxiliary annotations (e.g., loop invariants) into the program to facilitate the proofs. For complex properties or larger programs this quickly becomes the limiting factor for the applicability of current certification approaches.
Whalen, Michael↗