Software Specification and Verification Laboratory

Contact: Dr. Yoonsik Cheon

The goal of our research is to advance the practice of developing correct and reliable computer programs by making formal methods more accessible and practical for daily use. Formal methods, which are mathematical techniques used for the specification, development, and verification of computer programs, have been limited to high-integrity systems due to their high cost. We aim to expand their use by developing theories and techniques that are usable by professional programmers with limited mathematical backgrounds. Our research field, called operational formal methods, encompasses a range of practical and applicable tools, including specification languages, verification techniques, and support tools. By doing so, we hope to make formal methods a more integral part of the software development process.

Our research focuses on constructing correct programs that are formally proven or verified through verification and reasoning techniques. We utilize formally written design documents, such as OCL constraints, to build programs and have explored both static and dynamic verification methods. Our goal is to automatically translate OCL constraints into source code-level assertions or executable assertions. For this, our group has designed CleanJava, an annotation language for Java that supports Cleanroom-style functional program verification. In addition to our work in formal methods, we are now interested in applying established software engineering principles, techniques, and methods to the development of mobile applications, which are becoming increasingly popular and complex.

Dr. Cheon has made significant contributions to the field of specification language design, including the development of Larch/Smalltalk and participation in the design of Larch/C++. He also played a crucial role in the design and extension of the Java Modeling Language (JML), a formal specification language for Java, and developed essential tools such as the JML compiler. Dr. Cheon's work in inventing a connection between JML specifications and unit testing and developing an automated testing tool that uses the runtime assertion checking code as a test oracle has been widely recognized and has had a lasting impact on the field of formal methods and software engineering. His ECOOP 2002 publication was recognized with the AITO Test of Time Award at ECOOP 2022, which is a testament to the lasting impact of his work in the field. He has also extended this approach by automatically generating test data using various techniques, including random sampling, genetic algorithms, constraint solving, combinatorial techniques, and annotations.