CSE alumnus Zachary Tatlock (Ph.D. '14) is now a professor of computer science at the University of Washington. In an article about "hacker-proof coding" in the August issue of Communications of the ACM, the publication notes that as Tatlock was finishing up his dissertation at UC San Diego, the then-Ph.D. candidate gave a talk at UW about his thesis research on program verification (under his advisor, Sorin Lerner). The lead engineer for the UW medical center's radiotherapy team was in the audience and asked Tatlock how they could apply verification to that system.
professor at the University of Washington.
Recalling the event three years later, Tatlock reckons that the question "probably helped me get hired." He joined UW shortly after and has continued to work with the medical center. In the case of the radiotherapy system, he noted that because the system was written in a variety of languages, different techniques had to be deployed to verify the software in its entirety.
According to Esther Shein, who wrote the CACM article, "The system has about a dozen components, each with different levels of criticality." She quotes Tatlock saying that "software for logging an event, for example, is not as critical as software that verifies the beam power has not become too high. What we want to be able to do is ensure the reliability of all pieces. We want to make sure there are no bugs that can affect the parts that are critical."
The medical center wanted to prevent software errors that might prove fatal, given that the radiotherapy system "shoots high-powered radiation beams into the heads of patients to treat cancers of the tongue and esophagus," writes Shein. To check its heaviest-duty components, the medical center uses DeepSpec principles, which are costly and time-consuming because they require highly-trained technicians to prove they're functioning correctly.
To assess less-critical parts of the system, the medical center uses "lighter-weight, less powerful techniques to ensure the correctness," said Tatlock. "So the guarantees for those parts aren't as strong, but it's a better engineering trade-off."
The CACM article goes on to note that Tatlock and colleagues have built a suite of tools the engineers use in their regular development process. "They include a checker that allows them to formally describe the entire radiotherapy system to a computer and ensure the key components are individually correct. The researchers are now working on building verified replacements for those parts of the system." The system is also checked daily. "We want to make sure the code written by the engineers on that team will correctly turn off the beam if anything goes wrong," Tatlock told the publication. "The work is similar to DeepSpec's; it just emphasizes a different degree of automation."