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.

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.