Jonathan Jacky University of Washington Phone: 206-543-1720 Orthopaedics and Sports Medicine Fax: 206-685-8047 Box 356500 Email: jon@u.washington.edu Seattle, Washington 98195-6500 Web: http://staff.washington.edu/~jon/ Bibliography Books The Way of Z: Practical Programming with Formal Methods. Cambridge University Press, 1997. DIAC-87: Directions and Implications of Advanced Computing. (editor, with Doug Schuler) Ablex Publishing Corp., Norwood, N. J. 1989. Refereed Publications, sole author or first author Analyzing a real-time program with Z. In Jonathan Bowen, Andreas Fett, and Michael Hinchey, editors, ZUM '98: The Z Formal Specification Notation. Eleventh International Conference of Z Users, Springer-Verlag, 1998. Lecture Notes in Computer Science. (This analysis also used the SMV model checker.) Experience with Z developing a control program for a radiation therapy machine. (with Ruedi Risler and three other co-authors) In Jonathan P. Bowen, Michael G. Hinchey, and David Till, editors, ZUM '97: The Z Formal Specification Notation, pages 317 - 328. Tenth International Conference of Z Users, Springer-Verlag, 1997. Lecture Notes in Computer Science 1212. Modelling, checking, and implementing a control program for a radiation therapy machine. (with Michael Patrick) In Rance Cleaveland and Daniel Jackson, editors, AAS '97: Proceedings of the First ACM SIGPLAN Workshop on Automated Analysis of Software, pages 25 - 32, 1997. From Z to code: A graphical user interface for a radiation therapy machine. (with Jonathan Unger) In J. P. Bowen and M. G. Hinchey, editors, ZUM '95: The Z Formal Specification Notation, pages 315-333. Ninth International Conference of Z Users, Springer-Verlag, 1995. Lecture Notes in Computer Science 967. Specifying a safety-critical control system in Z. IEEE Transactions on Software Engineering, 21(2):99-106, 1995. Portable software tools for 3-D radiation therapy planning. (with 13 co-authors) International Journal of Radiation Oncology, Biology and Physics, 30(4):921-928, November 1994. Specifying a safety-critical control system in Z. In J. C. P. Woodcock and P. G. Larsen, editors, FME '93: Industrial-Strength Formal Methods, pages 388-402, Odense, Denmark, April 1993. First International Symposium of Formal Methods Europe, Springer-Verlag. Lecture Notes in Computer Science 670. Formal specification and development of control system input/output. In J. P. Bowen and J. E. Nicholls, editors, Z User Workshop, London 1992, pages 95-108. Proceedings of the Seventh Annual Z User Meeting, Springer-Verlag, Workshops in Computing Series, 1993. Formal specifications for a clinical cyclotron control system. In Mark Moriconi, editor, Proceedings of the ACM SIGSOFT International Workshop on Formal Methods in Software Development, pages 45-54, Napa, California, USA, May 9-11 1990. (Also in ACM Software Engineering Notes, 15(4), Sept. 1990). How to draw irregular radiation beams in 3D treatment plans. (with Ira Kalet) Computerized Medical Imaging and Graphics, 14(2):97-105, 1990. Testing a 3-D radiation therapy planning program. (with Cheryl White) International Journal of Radiation Oncology, Biology and Physics, 18:253-261, January 1990. An object-oriented programming discipline for standard Pascal. (with Ira Kalet) Communications of the ACM, 30(9):772-776, September 1987. An object-oriented approach to a large scientific application. (with Ira Kalet) In Norman Meyrowitz, editor, OOPSLA '86 Object Oriented Programming Systems, Languages and Applications Conference Proceedings, pages 368-376. Association for Computing Machinery, 1986. (also SIGPLAN Notices, 21(11), Nov. 1986). A general purpose data entry program. (with Ira Kalet) Communications of the ACM, 26(6):409-417, 1983. Barometric measurement of tidal volume: effects of pattern and nasal temperature. J. Appl. Physiol.: Respirat. Environ. Exercise Physiol. 49(2): 319-325, 1980. Programmable gas mixer for controlling concentration as a function of time. J. of Appl. Physiol.: Respirat. Environ. Exercise Physiol., 49(1):160-166, 1980. A plethysmograph for long-term measurements of ventilation in unrestrained animals. J. Appl. Physiol.: Respirat. Environ. Exercise Physiol. 45(4): 644-647, 1978. Invited publications, sole author Lessons from the formal development of a radiation therapy machine control program. In Michael G. Hinchey and Jonathan P. Bowen, editors, Industrial-Strength Formal Methods in Practice, pages 185-206. Springer-Verlag, 1999. Safety-critical computing: Hazards, practices, standards, and regulation. In Rob Kling, editor, Computerization and Controversy: Value Conflicts and Social Choices. Academic Press, 1996. (second edition). Safety of computer-controlled devices. In Developing Safe, Effective, and Reliable Medical Software. Association for the Advancement of Medical Instrumentation, Arlington, VA, 1991. Safety-critical computing: Hazards, practices, standards, and regulation. In Charles Dunlop and Rob Kling, editors, Computerization and Controversy: Value Conflicts and Social Choices. Academic Press, 1991. Risks in medical electronics. Communications of the ACM, 33(12):138, December 1990. 3-D radiation therapy treatment planning: Overview and assessment. American Journal of Clinical Oncology, 13(4):331-343, 1990. Quality assurance in medical computer systems. American Association of Physicists in Medicine Newsletter, 13(1):5-6, January/February 1988. Technical Reports, sole author or first author Prism DICOM-RT facility. (with Mark Phillips) Technical Report 2001-12-01, Radiation Oncology Department, University of Washington, Seattle, Box 356043, Seattle, Washington 98195-6043, USA, December 2001. A control system for a radiation therapy machine. (with Ruedi Risler, David Reid, Robert Emery, Jonathan Unger and Michael Patrick) Technical Report 2001-05-01, Radiation Oncology Department, University of Washington, Seattle, Box 356043, Seattle, Washington 98195-6043, USA, May 2001. Clinical neutron therapy system implementation. Technical Report 01-02-01, Department of Radiation Oncology, University of Washington, Box 356043, Seattle, Washington 98195-6043, USA, February 2001. Clinical neutron therapy system reference manual. (with Ruedi Risler) Technical Report 99-10-01, Department of Radiation Oncology, University of Washington, Box 356043, Seattle, Washington 98195-6043, USA, October 1999. Clinical neutron therapy system installation and operations. Technical Report 99-08-01, Department of Radiation Oncology, University of Washington, Box 356043, Seattle, Washington 98195-6043, USA, August 1999. Clinical neutron therapy system therapist's guide. (with Ruedi Risler) Technical Report 99-07-01, Department of Radiation Oncology, University of Washington, Box 356043, Seattle, Washington 98195-6043, USA, July 1999. Analyzing a real-time program with Z and SMV. Technical Report 98-06-01, Department of Radiation Oncology, University of Washington, Box 356043, Seattle, Washington 98195-6043, USA, June 1998. Formal specification of control software for a radiation therapy machine. (with Michael Patrick and Jonathan Unger) Technical Report 95-12-01, Radiation Oncology Department, University of Washington, Seattle, WA, December 1995. Clinical neutron therapy system, control system specification, Part III: Therapy console internals. (with Ruedi Risler and Michael Patrick) Technical Report 95-08-03, Radiation Oncology Department, University of Washington, Seattle, WA, August 1995. Formal specification of control software for a radiation therapy machine. (with Jonathan Unger) Technical Report 94-07-01, Radiation Oncology Department, University of Washington, Seattle, WA, July 1994. Formal specification and development of control system input/output (revised). Technical Report 92-11-02, Radiation Oncology Department, University of Washington, Seattle, WA, November 1992. Common Lisp language bindings to the foundation and virtual machine platform (VMP). (with Ira Kalet, Michael Kahn, and Steve Cousins) Technical Report 92-2, National Cancer Institute, Radiation Research Program, 6120 Executive Boulevard, Executive Plaza North, Rockville MD 20852, 1992. Report of the Radiotherapy Treatment Planning Tools Implementation Task Group. ANSI C language bindings to the foundation and virtual machine platform (VMP). (with Gregg Tracton, Di Yan, and William Harms) Technical Report 92-1, National Cancer Institute, Radiation Research Program, 6120 Executive Boulevard, Executive Plaza North, Rockville MD 20852, 1992. Report of the Radiotherapy Treatment Planning Tools Implementation Task Group. Specifying a safety-critical control system in Z. Technical Report 92-09-02, Radiation Oncology Department, University of Washington, Seattle, WA, September 1992. Clinical neutron therapy system, control system specification, Part II: User operations. (with Ruedi Risler, Ira Kalet, Peter Wootton, and Stan Brossard) Technical Report 92-05-01, Radiation Oncology Department, University of Washington, Seattle, WA, May 1992. Verification, analysis and synthesis of safety interlocks. Technical Report 91-04-01, Radiation Oncology Department, University of Washington, Seattle, WA, April 1991. Using formal models to plan control system testing. (with Alexandra Barke and Ruedi Risler) Technical Report 91-02-02, Radiation Oncology Department, University of Washington, Seattle, WA, February 1991. Foundation library specification and virtual machine platform (VMP) specification. (with eight co-authors) Technical Report 91-1, National Cancer Institute, Radiation Research Program, 6120 Executive Boulevard, Executive Plaza North, Rockville MD 20852, 1991. Report of the Radiotherapy Treatment Planning Tools Specification Task Group. Clinical neutron therapy system, control system specification, Part I: System overview and hardware organization. (with Ruedi Risler, Ira Kalet, and Peter Wootton) Technical Report 90-12-01, Radiation Oncology Department, University of Washington, Seattle, WA, December 1990. Publications about public affairs, history, and for the general reader Programmed for disaster: software errors that imperil lives. The Sciences 29(5): 22 - 27, September/October 1989. The DARPA Strategic Computing Program. In: D. Bellin and G. Chapman, eds.: Computers in Battle: Will They Work?, Harcourt Brace Jovanovich 1987. Ada's troubled debut. The Sciences January/February 1987. The ``Star Wars'' Defense Won't Compute. The Atlantic Monthly, June 1985. Software and web pages Foundations of Computing (course notes) http://grace.evergreen.edu/~jackyj/fofc/fofc.html Data Structures and Algorithms (course notes) http://grace.evergreen.edu/~jackyj/dsa/dsa.html Z2HTML translator (software and documentation) http://www.radonc.washington.edu/prostaff/jon/z/z2html/z2html.html Clinical Neutron Therapy System (links to reports and publications) http://www.radonc.washington.edu/physics/cnts/ Radiotherapy Treatment Planning Tools (links to reports, publications and code) http://www.radonc.washington.edu/medinfo/rtpt/ Unrefereed publications, sole author or first author (conference proceedings, etc.) Formal safety analysis of the control program for a radiation therapy machine. In Wolfgang Schlegel and Thomas Bortfeld, editors, The Use of Computers in Radiation Therapy: XIIIth International Conference, pages 68-70. Springer, 2000. Designing software for a radiation therapy machine in a formal notation. (with J. Unger) In M. Wirsing, editor, ICSE-17 Workshop on Formal Methods Application in Software Engineering Practice, pages 14-21, 1995. Formal specification of control software for a radiation therapy machine. (with J. Unger) In: A. R. Hounsel, J. M. Wilkinson, and P. C. Williams (Eds)., Eleventh International Conference on the Use of Computers in Radiation Therapy Proceedings, Medical Physics Publishing, Madison WI, 1994, pages 216 - 217. Networked computer control systems for radiation therapy. (with I. Kalet) In: A. R. Hounsel, J. M. Wilkinson, and P. C. Williams (Eds)., Eleventh International Conference on the Use of Computers in Radiation Therapy Proceedings, Medical Physics Publishing, Madison WI, 1994, pages 52 - 53. Formal specifications for a cyclotron control system. (withR. Risler) In G. Dutton and M. K. Cradduck, editors, Proceedings of the Thirteenth International Conference on Cyclotrons and Their Applications, pages 689-692. World Scientific, 1992. Control system specification for a cyclotron and neutron therapy facility. (with Ruedi Risler, Ira Kalet, Peter Wootton, Alexandra Barke, Stan Brossard, and Ralph Jackson) In Conference Record of the 1991 IEEE Particle Accelerator Conference: Acclerator Science and Technology, pages 1359-1361, San Francisco, California, May 1991. IEEE Press. Relational database: a radiation therapy machine control software development tool. (with R. Risler, S. Brossard, and I. Kalet.) In Yongmin Kim and Francis A. Spelman, editors, Images of the Twenty-First Century: Proceedings of the Annual International Conference of the IEEE Engineering in Medicine and Biology Society, Volume 11, pages Part 6, 1918-1919, 1989. Assuring the quality of critical software. (with Ira Kalet) In I. A. D. Bruinvis, P. H. van der Giessen, H. J. van Kleffens, and F. W. Wittkämper, editors, Proceedings of the Ninth International Conference on the Use of Computers in Radiation Therapy, pages 49-52, Amsterdam, 1987. North-Holland. COMPASS '88 trip report. ACM Software Engineering Notes, 13(4):21-27, Oct 1988. Abstracts, sole author or first author Portable software tools for 3D radiation therapy planning. (with the NCI Radiotherapy Treatment Planning Tools Working Group) International Journal of Radiation Oncology, Biology and Physics, 27 (Suppl. 1), 1993, p. 182. Control system specification for a cyclotron and neutron therapy facility. (with Risler, R., Kalet, I., Wootton, P., Barke, A., Brossard, S., and Jackson, R.)Medical Physics 18, 627, 1991. Use of concurrent processes in treatment plan display. (with Kalet, I.)Medical Physics 9, 615, 1982. Effects of sleep state on ventilation and CO2 responses in the infant monkey. The Physiologist 21: 59, 1978. Ventilatory responses to inhaled CO2 during sleep in the infant primate. Diss. Abstr. B. Sci. Eng. 1: 122, 1978. Refereed Publications, co-author Integration of radiotherapy planning systems and radiotherapy treatment equipment: 11 years experience. Ira J. Kalet, Jonathan P. Jacky, Ruedi Risler, Solveig Rohlin, and Peter Wootton. International Journal of Radiation Oncology, Biology and Physics, 38(1):213-221, 1997. Automated planning target volume generation: An evaluation pitting a computer-based tool against human experts. Case H. Ketting, Mary M. Austin-Seymour, Ira J. Kalet, Jonathan P. Jacky, Sharon E. Kromhout-Schiro, Sharon M. Hummel, Jonathan M. Unger, Lawrence M. Fagan, and Thomas W. Griffin. International Journal of Radiation Oncology, Biology and Physics, 37(3):697-704, 1997. Consistency of three-dimensional planning target volumes across physicians and institutions. Case H. Ketting, Mary M. Austin-Seymour, Ira J. Kalet, Jonathan M. Unger, Sharon M. Hummel, and Jonathan P. Jacky. International Journal of Radiation Oncology, Biology and Physics, 37(2):445-453, 1997. Prism: A new approach to radiotherapy planning software. Ira J. Kalet, Jonathan P. Jacky, Mary M. Austin-Seymour, Sharon M. Hummel, Kevin J. Sullivan, and Jonathan M. Unger. International Journal of Radiation Oncology, Biology and Physics, 36(2):451-461, 1996. Evaluation of an expert system producing geometric solids as output. Case H. Ketting, Mary M. Austin-Seymour, Ira J. Kalet, Jonathan P. Jacky, Sharon E. Kromhout-Schiro, Sharon M. Hummel, Jonathan M. Unger, and Lawrence M. Fagan. In Reed M. Gardner, editor, Proceedings of the Nineteenth Annual Symposium on Computer Applications in Medical Care, pages 683-687, Philadelphia, PA, 1995. Hanley and Belfus, Inc. Three-dimensional planning target volumes: A model and a software tool. Mary Austin-Seymour, Ira Kalet, John McDonald, Sharon Kromhout-Schiro, Jon Jacky, Sharon Hummel, and Jonathan Unger. International Journal of Radiation Oncology Biology Physics, 33(5):1073-1080, 1995. Impact of a multileaf collimator on treatment morbidity in localized carcinoma of the prostate. Mary Austin-Seymour, Richard Caplan, Kenneth Russell, George Laramore, Jon Jacky, Peter Wootton, Sharon Hummel, Karen Lindsley, and Thomas Griffin. International Journal of Radiation Oncology Biology Physics, 30(5):1065-1071, Dec 1994. Boron neutron capture therapy: A mechanism for achieving a concomitant tumor boost in fast neutron radiotherapy. George E. Laramore, Peter Wootton, John C. Livesey, Donald S. Wilbur, Ruedi Risler, Mark Phillips, Jon Jacky, Thomas A. Buchholz, Thomas W. Griffin, and Stanley Brossard. International Journal of Radiation Oncology, Biology and Physics, 28(5):1135-1142, 1994. Enhancement of fast neutron beams with boron neutron capture therapy. Thomas A. Buchholz, George E. Laramore, Peter Wootton, John C. Livesey, D. Scott Wilbur, Ruedi Risler, John Jacky, and Thomas W. Griffin. Acta Oncologica, 33(3):307-313, 1994. Software design for interactive graphic radiation treatment simulation systems. Ira J. Kalet, Christine Sweeney, and Jonathan P. Jacky. In Randolph A. Miller, editor, Proceedings of the Fourteenth Annual Symposium on Computer Applications in Medical Care, pages 594-598. IEEE Computer Society Press, 1990. Radiotherapy planning: direct tumor location on simulation and port films using CT. Haynor, D.R., A.W. Borning, B.A. Griffin, J.P. Jacky, I.J. Kalet, and W.P. Shuman. Radiology 158: 537 - 540, 1986. A research-oriented treatment planning program system. Ira J. Kalet and Jonathan P. Jacky. Computer Programs in Biomedicine, 14:85-98, 1982. Left ventricular performance in endotoxin shock in dogs. Am. J. Physiol Guntheroth, W.G., J.P. Jacky, I. Kawabori, J.G. Stevenson, and A.H. Moreno. 242 (Heart Circ. Physiol. 11): H172-H176, 1982. Invited publications, co-author Special section on computing and social responsibilities: Introduction. Schuler, Douglas and Jacky, Jonathan. Communications of the ACM 32(8): 925 - 927, 1989. The effects of respiration on venous return, pleural and pericardial pressure. Guntheroth, W.G. and J.P. Jacky. In, Pericardial Disease, ed. by P.S. Reddy, Raven Press, New York, pps. 137-147, 1982. Technical Reports, co-author Prism user's reference manual, version 1.3. Ira J. Kalet, Mark H. Phillips, Jonathan P. Jacky and Robert S. Giansiracusa. Technical Report 2000-07-01, Radiation Oncology Department, University of Washington, Seattle, Washington, 2000. Prism dose computation methods, version 1.3. Ira J. Kalet, Gavin Young, Robert Giansiracusa, Paul Cho, and Jonathan Jacky. Technical Report 2000-04-01, Radiation Oncology Department, University of Washington, Seattle, Washington, 2000. Prism system implementation, version 1.2. Ira J. Kalet, Jonathan Unger, and Jonathan Jacky. Technical Report 99-mm-nn, Radiation Oncology Department, University of Washington, Seattle, Washington, 1998. Prism system capabilities and user interface specification, version 1.2. Ira J. Kalet, Jonathan Unger, Jonathan Jacky, and Mark Phillips. Technical Report 97-12-02, Radiation Oncology Department, University of Washington, Seattle, Washington, 1997. Prism dose computation methods, version 1.2. Ira J. Kalet, Gavin Young, Robert Giansiracusa, Jonathan Jacky, and Paul Cho. Technical Report 97-12-01, Radiation Oncology Department, University of Washington, Seattle, Washington, 1997. Prism system implementation, version 1.1. Ira J. Kalet, Jonathan Unger, and Jonathan Jacky. Technical Report 95-09-01, Radiation Oncology Department, University of Washington, Seattle, Washington, 1995. Prism system capabilities and user interface specification, version 1.1. Ira J. Kalet, Jonathan Unger, Jonathan Jacky, and Mark Phillips. Technical Report 95-08-01, Radiation Oncology Department, University of Washington, Seattle, Washington, 1995. CT image transfer service. Jonathan Unger and Jonathan Jacky. Technical Report 94-07-02, Radiation Oncology Department, University of Washington, 1994. CT image unpacking/preparation utilities. Jonathan Unger and Jonathan Jacky. Technical Report 94-07-01, Radiation Oncology Department, University of Washington, 1994. Prism dose computation methods. Ira J. Kalet, Jonathan Jacky, Paul Cho, and Mark Martin. Technical Report 93-09-01, Radiation Oncology Department, University of Washington, Seattle, Washington, 1993. Prism system capabilities and user interface specification, version 1.0. Ira J. Kalet, Jonathan Unger, Jonathan Jacky, and Mark Phillips. Technical Report 93-08-02, Radiation Oncology Department, University of Washington, Seattle, Washington, 1993. Prism graphical user interface specification. Ira J. Kalet, Jonathan Unger, Christine Sweeney, , Sharon Hummel, Jonathan Jacky, and Mark Niehaus. Technical Report 92-02-02, Radiation Oncology Department, University of Washington, Seattle, Washington, 1992. The prism radiation treatment planning system. Ira J. Kalet, Jonathan Jacky, Sharon Kromhout-Schiro, Brian Lockyear, Mark Niehaus, Christine Sweeney, and Jonathan Unger. Technical Report 91-10-03, Radiation Oncology Department, University of Washington, Seattle, Washington, 1991. UWPLAN dose computation methods. Ira J. Kalet and Jonathan P. Jacky. Technical Report 91-02-01, University of Washington, 1991. Unrefereed publications, co-author Clinical applications of a DSI based simulator. P. S. Cho, J. P. Jacky, and T. W. Griffin. In R. F. Mould, editor, International Radiotherapy Review, pages 39-50, Linac House, Fleming Way, Crawley, West Sussex RH10 2RR UK, 1995. Philips 1995 International Radiotherapy Users' Meeting, Philips Medical Systems -- Radiotherapy. Continued operation of the Seattle clinical cyclotron facility. Risler, R. and Jacky, J. In: G. Dutto and M. K. Cradduck (Eds.), Cyclotrons and Their Applications: Proceedings of the Thirteenth International Conference, Vancouver, 1992. Singapore, World Scientific 1993, pages 262 - 265. Boron neutron capture: A means of increasing the effectiveness of fast neutron radiotherapy. G. E. Laramore, J. C. Livesey, P. Wootton, D. S. Wilbur, J. Jacky, R. Risler, and R. Vesella. In W. C. Dewey, M. Edington, R. J. M. Fry, E. J. Hall, and G. F. Whitmore, editors, Proceedings of the Ninth International Conference on Radiation Research, Toronto, Canada, July 1991. Academic Press. Routine operation of the Seattle cyclotron facility. R. Risler, S. Brossard, J. Eenmaa, J. Jacky, I. Kalet, A. Rask, and P. Wootton. In B. Martin and K. Ziegler, editors, Cyclotrons and Their Applications: Proceedings of the Twelfth International Conference, Berlin, FR Germany, 8 - 12 May 1989, Singapore, 1991. World Scientific Publishing Co. Knowledge-based computer simulation for radiation therapy planning. Kalet, I.J. and Jacky, J.P. In: I.A.D. Bruinvis, P.H. van der Giessen, H.J. van Kleffens, F.W. Wittkamper, eds., Proceedings of the 9th International Conference on the Use of Computers in Radiation Therapy. Amsterdam, North-Holland, 1987. pps. 553 - 556. Installation of the cyclotron based clinical neutron therapy system in Seattle. Ruedi Risler, Jüri Eenmaa, Jonathan P. Jacky, Ira J. Kalet, Peter Wootton, and S. Lindbaeck. In Proceedings of the Tenth International Conference on Cyclotrons and their Applications, pages 428-430, East Lansing, Michigan, May 1984. IEEE. Abstracts, co-author A multi-institutional evaluation of dose-volume histogram calculations. Harms, W. B., Purdy, J. A. and the members of the 3D CRT Collaborative Group. Medical Physics 21(6), June 1994, p. 927. 1994. Initial developments in a portable software tool which creates target volumes for treatment planning. Kromhout-Schiro, S., Austin-Seymour, M., Kalet, I. and Jacky, J. Medical Physics 18, 626, 1991. A version of this bibliography with links to many online publications is at http://staff.washington.edu/~jon/jacky-bib.html A resume with links to projects and selected online publications is at http://staff.washington.edu/~jon/jacky-resume.html