An official website of the United States government
Physical demonstration of vitrification of liter scale CPA systems and characterization of 120KW RF coil for nanowarming of liter scale systems
- Award ID(s):
- 1941543
- PAR ID:
- 10637016
- Publisher / Repository:
- Cryobiology
- Date Published:
- Journal Name:
- Cryobiology
- Volume:
- 109
- Issue:
- C
- ISSN:
- 0011-2240
- Page Range / eLocation ID:
- 37
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
Hybrid photonic integration provides a platform to design and implement novel functionalities unavailable to active or passive material systems alone. We present an automated alignment and assembly process for hybrid-integrated laser systems, comprising silicon nitride (Si3N4) photonic integrated circuits (PICs) edge-coupled to gallium arsenide (GaAs) gain chips (GCs). We design and optimize spot size converters (SSCs) to increase the alignment tolerances between the PICs and GCs. Our automated assembly process has achieved experimental coupling losses of 2.7 dB between the PICs and GCs, closely matching the simulated values. Packaged hybrid lasers, when coupled to a lensed fiber, exhibit slope efficiencies of ∼ 97 mW/A. These results show the feasibility of scaling the production and widespread application of these hybrid laser systems by automating their assembly, which should drive down packaging costs and accelerate research.more » « less
-
Reasoning about memory aliasing and mutation in software verification is a hard problem. This is especially true for systems using SMT-based automated theorem provers. Memory reasoning in SMT verification typically requires a nontrivial amount of manual effort to specify heap invariants, as well as extensive alias reasoning from the SMT solver. In this paper, we present a hybrid approach that combines linear types with SMT-based verification for memory reasoning. We integrate linear types into Dafny, a verification language with an SMT backend, and show that the two approaches complement each other. By separating memory reasoning from verification conditions, linear types reduce the SMT solving time. At the same time, the expressiveness of SMT queries extends the flexibility of the linear type system. In particular, it allows our linear type system to easily and correctly mix linear and nonlinear data in novel ways, encapsulating linear data inside nonlinear data and vice-versa. We formalize the core of our extensions, prove soundness, and provide algorithms for linear type checking. We evaluate our approach by converting the implementation of a verified storage system (about 24K lines of code and proof) written in Dafny, to use our extended Dafny. The resulting system uses linear types for 91% of the code and SMT-based heap reasoning for the remaining 9%. We show that the converted system has 28% fewer lines of proofs and 30% shorter verification time overall. We discuss the development overhead in the original system due to SMT-based heap reasoning and highlight the improved developer experience when using linear types.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Journal Article:
- https://doi.org/10.1016/j.cryobiol.2022.11.118
