More Like this

1. Body‐loop related MRI radiofrequency‐induced heating hazards: Observations, characterizations, and recommendations

   https://doi.org/10.1002/mrm.28954  

   Yang, Xiaolin; Zheng, Jianfeng; Wang, Yu; Long, Stuart A.; Kainz, Wolfgang; Chen, Ji (August 2021, Magnetic Resonance in Medicine)

   PurposeTo assess RF‐induced heating hazards in 1.5T MR systems caused by body‐loop postures. MethodsTwelve advanced high‐resolution anatomically correct human body models with different body‐loop postures are created based on poseable human adult male models. Numerical simulations are performed to assess the radiofrequency (RF)‐induced heating of these 12 models at 11 landmarks. A customized phantom is developed to validate the numerical simulations and quantitatively analyze factors affecting the RF‐induced heating, eg, the contact area, the loop size, and the loading position. The RF‐induced heating inside three differently posed phantoms is measured. ResultsThe RF‐induced heating from the body‐loop postures can be up to 11 times higher than that from the original posture. The RF‐induced heating increases with increasing body‐loop size and decreasing contact area. The magnetic flux increases when the body‐loop center and the RF coil isocenter are close to each other, leading to increased RF‐induced heating. An air gap created in the body loop or generating a polarized magnetic field parallel to the body loop can reduce the heating by a factor of three at least. Experimental measurements are provided, validating the correctness of the numerical results. ConclusionSafe patient posture during MR examinations is recommended with the use of insulation materials to prevent loop formation and consequently avoiding high RF‐induced heating. If body loops cannot be avoided, the body loop should be placed outside the RF transmitting coil. In addition, linear polarization with magnetic fields parallel to the body loop can be used to circumvent high RF‐induced heating. 

   more » « less
2. I4: incremental inference of inductive invariants for verification of distributed protocols

   https://doi.org/10.1145/3341301.3359651  

   Ma, Haojun; Goel, Aman; Jeannin, Jean-Baptiste; Kapritsos, Manos; Kasikci, Baris; Sakallah, Karem A. (October 2019, Proceedings of the 27th ACM Symposium on Operating Systems Principles)

   Designing and implementing distributed systems correctly is a very challenging task. Recently, formal verification has been successfully used to prove the correctness of distributed systems. At the heart of formal verification lies a computer-checked proof with an inductive invariant. Finding this inductive invariant, however, is the most difficult part of the proof. Alas, current proof techniques require inductive invariants to be found manually—and painstakingly—by the developer. In this paper, we present a new approach, Incremental Inference of Inductive Invariants (I4), to automatically generate inductive invariants for distributed protocols. The essence of our idea is simple: the inductive invariant of a finite instance of the protocol can be used to infer a general inductive invariant for the infinite distributed protocol. In I4, we create a finite instance of the protocol; use a model checking tool to automatically derive the inductive invariant for this finite instance; and generalize this invariant to an inductive invariant for the infinite protocol. Our experiments show that I4 can prove the correctness of several distributed protocols like Chord, 2PC and Transaction Chains with little to no human effort. 

   more » « less
3. Data-Driven Invariant Learning for Probabilistic Programs

   https://doi.org/10.1007/978-3-031-13185-1_3  

   Bao, Jialu; Trivedi, Nitesh; Pathak, Drashti; Roy, Subhajit (January 2022, Lecture notes in computer science)

   Shoham, Sharon; Vizel, Yakir (Ed.)

   Morgan and McIver’s weakest pre-expectation framework is one of the most well-established methods for deductive verification of probabilistic programs. Roughly, the idea is to generalize binary state assertions to real-valued expectations, which can measure expected values of probabilistic program quantities. While loop-free programs can be analyzed by mechanically transforming expectations, verifying loops usually requires finding an invariant expectation, a difficult task. We propose a new view of invariant expectation synthesis as a regression problem: given an input state, predict the average value of the post-expectation in the output distribution. Guided by this perspective, we develop the first data-driven invariant synthesis method for probabilistic programs. Unlike prior work on probabilistic invariant inference, our approach can learn piecewise continuous invariants without relying on template expectations. We also develop a data-driven approach to learn sub-invariants from data, which can be used to upper- or lower-bound expected values. We implement our approaches and demonstrate their effectiveness on a variety of benchmarks from the probabilistic programming literature. 

   more » « less
4. Reflections on Termination of Linear Loops

   https://doi.org/10.1007/978-3-030-81688-9_3  

   Zhu, Shaowei; Kincaid, Zachary (July 2021, Computer Aided Verification)

   This paper shows how techniques for linear dynamical systems can be used to reason about the behavior of general loops. We present two main results. First, we show that every loop that can be expressed as a transition formula in linear integer arithmetic has a best model as a deterministic affine transition system. Second, we show that for any linear dynamical system f with integer eigenvalues and any integer arithmetic formula G, there is a linear integer arithmetic formula that holds exactly for the states of f for which G is eventually invariant. Combining the two, we develop a monotone conditional termination analysis for general loops. 

   more » « less
5. Automaton-based Implicit Controlled Invariant Set Computation for Discrete-Time Linear Systems

   https://doi.org/10.1109/CDC45484.2021.9683574  

   Liu, Zexiang; Anevlavis, Tzanis; Ozay, Necmiye; Tabuada, Paulo (December 2021, IEEE Conference on Decision and Control)

   In this paper, we derive closed-form expressions for implicit controlled invariant sets for discrete-time controllable linear systems with measurable disturbances. In particular, a disturbance-reactive (or disturbance feedback) controller in the form of a parameterized finite automaton is considered. We show that, for a class of automata, the robust positively invariant sets of the corresponding closed-loop systems can be expressed by a set of linear inequality constraints in the joint space of system states and controller parameters. This leads to an implicit representation of the invariant set in a lifted space. We further show how the same parameterization can be used to compute invariant sets when the disturbance is not available for measurement. 

   more » « less