LIAMALOGO

FCST: Formally Certified Software Tools

Updated: 2019/1/31   

 Scientific leaders: Dr. Jean-François MONIN (UGA/CNRS); Dr. Shengyuan WANG (Tsinghua)

 
LIAMA founding members involved: UGA/CNRS (France), Tsinghua (China)
 
Creation: 2016
 
Project Description 
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 [1] and would be released in the near future [2]. 
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. [3]
 
References
[1] Open source version of L2C, available at
 http://soft.cs.tsinghua.edu.cn/~wang/projects/L2C/sources/open-l2c-1.0-Beta.zip 
[2] Open L2C home: http://soft.cs.tsinghua.edu.cn:8000/
[3] 核安全级应用软件集成开发工具的研制与应用,北京广利核系统工程有限公司、清华大学、阳江核电有限公司,2018年中国产学研合作创新成果奖一等奖. 人员:任保华、张智慧、杨晨、王生原、江国进、石桂连、吕秀红、董渊、汤凌、赵锋。
 
For the details, please refer to http://soft.cs.tsinghua.edu.cn:8000/

 

回首页 回前页 回到页首