Cryocooler cooled superconducting magnets using Bismuth based high-Tc current leads have been successfully demonstrated. The magnets mainly consisted of a superconducting coil, current leads and a radiation shield which are cooled by a two stage Gifford-McMahon cryocooler without using liquid helium. Our first liquid helium-free 4.6 T (Nb, Ti)3Sn superconducting magnet with a room temperature bore of 38 mm operated at 11 K has recorded a continuous operation at 3.7 T for 1,200 hours and total cooling time over 10,000 hours without trouble. As a next step, we constructed a (Nb, Ti)3Sn liquid helium-free superconducting magnet with a wider room temperature bore of 60 mm. The coil temperature reached 8.3 K in 37 hours after starting the cryocooler. The magnet generated 5.0 T at the center of the 60 mm room temperature bore at an operating current of 140 A. An operation at a field of 5 T was confirmed to be stable even if the cryocooler has been stopped for 4 minutes. These results show that the liquid helium-free superconducting magnets can provide an excellent performance for a new application of the superconducting magnet.

This paper proposes a model checking method for microcomputer programs. To deal with the state explosion problem, we adopt a compositional verification approach. Based on the proposed method, a microcomputer program for a real-life air-conditioner is verified. The program is large enough to cause state explosion. Among fourteen typical properties of the program, five properties are successfully verified by our method.