Search for: All records

Because of the probabilistic/nondeterministic behavior of quantum programs, it is highly advisable to verify them formally to ensure that they correctly implement their specifications. Formal verification, however, also traditionally requires significant effort. To address this challenge, we present Qafny, an automated proof system based on the program verifier Dafny and designed for verifying quantum programs. At its core, Qafny uses a type-guided quantum proof system that translates quantum operations to classical array operations modeled within a classical separation logic framework. We prove the soundness and completeness of our proof system and implement a prototype compiler that transforms Qafny programs and specifications into Dafny for automated verification purposes. We then illustrate the utility of Qafny’s automated capabilities in efficiently verifying important quantum algorithms, including quantum-walk algorithms, Grover’s algorithm, and Shor’s algorithm. 

This paper presents a state-variable formulation to model and simulate the 2D unsteady aerodynamics of an airfoil undergoing arbitrary motion kinematics. The model builds upon a large-angle unsteady aerodynamic formulation in which the airfoil is represented using a lumped vortex element (LVE) model. The airfoil is divided into several panels, with a bound vortex placed on each panel. At any time instant, the bound-vortex strengths are determined by employing zero-normal-flow conditions at the control points located on each panel. The vorticity shed from the trailing edge of the airfoil is modeled using discrete vortices that move freely in the flow field. The required state variables are first identified, and all the time derivative terms of the state variables are then derived to form the final state-variable representation. Trailing-edge vortex shedding is incorporated using the Kelvin condition. The final state variable equation can be solved as an ordinary differential equation using any standard ODE-solving algorithm. Three case studies are presented here to evaluate the predictions of the model. In the cases considered here, the airfoil undergoes various unsteady plunge motions. The aerodynamic load history and the wake patterns are compared against the results from the low-order model developed by Narsipur et al. [1] in previous research. The comparison shows that the current state-variable formulation captures the unsteady flow characteristics and the aerodynamic load in good agreement with the reference results. 

Background:Cardiac regeneration after injury is limited by the low proliferative capacity of adult mammalian cardiomyocytes (CMs). However, certain animals readily regenerate lost myocardium through a process involving dedifferentiation, which unlocks their proliferative capacities. Methods:We bred mice with inducible, CM-specific expression of the Yamanaka factors, enabling adult CM reprogramming and dedifferentiation in vivo. Results:Two days after induction, adult CMs presented a dedifferentiated phenotype and increased proliferation in vivo. Microarray analysis revealed that upregulation of ketogenesis was central to this process. Adeno-associated virus-driven HMGCS2 overexpression induced ketogenesis in adult CMs and recapitulated CM dedifferentiation and proliferation observed during partial reprogramming. This same phenomenon was found to occur after myocardial infarction, specifically in the border zone tissue, and HMGCS2 knockout mice showed impaired cardiac function and response to injury. Finally, we showed that exogenous HMGCS2 rescues cardiac function after ischemic injury. Conclusions:Our data demonstrate the importance of HMGCS2-induced ketogenesis as a means to regulate metabolic response to CM injury, thus allowing cell dedifferentiation and proliferation as a regenerative response.