Professor Cheon's main research area is formal aspects of software development: requirement, design, programming, testing, verification and validation. Modern software development requires the design and analysis of a number of different artifacts. Formal techniques and methods allow the mathematically precise formulation of these artifacts. His main research goal is to enable a wider use of formal techniques and methods. This involves developing theories and techniques usable by software developers and programmers with minimal mathematical background. He calls his research field "operational formal methods"---formal methods that are practical and applicable to daily software development and programming work. These include, but are not limited to, specification languages, verification and validation techniques, programming languages, programming methodologies, and support tools. Dr. Cheon participated and worked in the design and implementation of several formal specification languages and their support tools, including Larch/C++, Larch/Smalltalk, Java Modeling Language (JML), and CleanJava.Dr. Cheon earned his BS from Korea University, and his masters and doctoral degrees from Iowa State University. He spent eight years on the research staff of the Computer and Software Technology Laboratory at the Electronics and Telecommunications Research Institute (ETRI), Taejon, South Korea.