Yoonsik Cheon's Research Overview

My research philosophy is to produce research that advances the practice of developing correct and reliable computer programs. I strongly advocate that formal methods---mathematically-based techniques for the specification, development and verification of computer programs---should play an important role in the development of computer programs. However, the high cost associated with formal methods has limited their use only to the development of high-integrity systems. My research goal is to enable a wider use of formal methods. This involves developing theories and techniques usable by practicing programmers with minimal mathematical background. I call my research field operational formal methods---formal methods that are practical and applicable to real-life programming. These include, but are not limited to, specification languages, verification and reasoning techniques, and support tools.

• Operational principles. The key research question is: what makes formal methods operational? What paradigms of specification notations and semantics, what kinds of verification and reasoning techniques, and what kinds of support tools can be called operational? Empirical studies will be an important tool for my research in this area. Guided by my findings I would also like to make existing techniques and approaches more operational or to define a whole new approach that is operational.
• Operational notations. I am very much interested in designing specification notations and languages, in particular, behavioral interface specification languages that can document in detail the behaviors of program modules. Ideally, an operational specification language should have notations and semantics that are familiar with and intuitive to programmers. My experience in these areas is broad, ranging from algebraic specification languages, process algebra, model-oriented languages, to component and architectural description languages. In particular, I have designed Larch/Smalltalk and co-designed Larch/C++. My work on the Java Modeling Language (JML) has a heavy influence on my view on operational specification languages; a programming language's expressions with a suitable extension can be successfully used as specification constructs with an added benefit of executability.
• Operational techniques. An important part of my research in operational form al methods is to develop techniques and approaches utilizing operational specifications to improve the quality of software and the productivity of programmers. Promising in this area are automated verification approaches amenable to programmers such as runtime assertion checking and assertion-based testing.
• Operational support tools. As I am an experimentalist, it has always been a part of my research to design and implement practical tools, e.g., a runtime assertion checker for JML and a JML-JUnit testing tool. Formal methods tools that give immediate and tangible payoff appeal more to programmers.

To summarize, my research interests, experience, and future directions are broadly spread over all the fields of what I refer to as operational formal methods, and I am excited about pursuing researches in these areas and look forward to collaborating with other people who share the same vision of practical application of formal methods.

Last modified: $Id: overview.html,v 1.3 2009/03/06 06:42:36 cheon Exp $