The goal of the project FCST is to address the application of formal methods applied to the formal certification of open-source software tools. Specifically, we mainly focused on developing two types of tools: (1) a certified compiler for the Lustre language, targetting the C language; (2) static checkers for some kinds of inconsistent or unsafe behaviors of key component of operating systems such as file systems, network protocol stacks and device drivers.
Supported partially from FCST, the certified compiler for a Lustre-like language, called L2C, has been developing into an open source version  and would be released in the near future .
Thanks to the project FCST, the members shared some meaningful and interesting academic activities, and also made some publications and awards.
Publications and Awards
1. Shi G, Zhang Y C, Shang S, Wang S Y, Dong Y, Yew P C. A formally verified transformation to unify multiple nested clocks for a Lustre-like language. Science China Information Sciences, 2019, 62(1). doi: 10.1007/s11432-016-9270-0.
2. Youren Shen, Yu Chen, Kang Chen, Hongliang Tian and Shoumeng Yan (Intel)，To Isolate, or to Share? That is a Question for Intel SGX, APSys 2018.
3. Yanjie Zhen, Wei Zhang, Zhenyang Dai, Junjie Mao and Yu Chen, Is It Possible to Automatically Port Kernel Modules? APSys 2018.
4. Shi, G., Gan, Y., Shang, S., Wang, S., Dong, Y., & Yew, P. C. A formally verified sequentializer for lustre-like concurrent synchronous data-flow programs. In Proceedings - 2017 IEEE/ACM 39th International Conference on Software Engineering Companion, ICSE-C 2017 (pp. 109-111).
5. Shang S, Gan YK, Shi G, Wang SY, Dong Y. Key Translations of the Trustworthy Compiler L2C and Its Design and Implementation[J]. Journal of Software, 2017, 28(5): 1233-1246(in Chinese).http://www.jos.org.cn/1000-9825/5213.htm.
6. An application of the research related to L2C compiler received an award from China Association for Promoting Industry-University-Research Cooperation.