Software Specification and Verification Laboratory

Contact: Dr. Yoonsik Cheon

Our research philosophy is to produce research that advances the practice of developing correct and reliable computer programs. We 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. Our research goal is to enable wider use of formal methods. This involves developing theories and techniques usable by professional programmers with minimal mathematical background. We call our research field operational formal methods -- formal methods that are practical and applicable to daily programming. These include, but are not limited to, specification languages, verification and reasoning techniques, and support tools. We recently become interested in applying established software engineering principles, techniques, and methods to mobile application developments, as mobile applications grow in popularity and complexity.

Projects

Other Links


Last modified: $Id: index.html,v 1.48 2019/08/17 18:55:40 cheon Exp $