I recruit 2-3 graduate students (Combined MS-PhD Program) each year.
Warning: we are working in the fields of theoretical computer science, with an emphasis on application in system safety and security.
A strong interest in our research plus ambitious with good programming skills, solid mathematical background, clear future plan is desired.
If you really interested, do not hesitate to drop me a mail with your CV and a brief research statement (about your research experience and plan). Potential candidates are encouraged to participate in the ShanghaiTech summer camp at the end of their junior year. For more information about our graduate program, please see http://sist.shanghaitech.edu.cn/cn/gsr
You will implement prepared algorithms that solve problems on programs or systems verification. Programming languages are optional. It is a good opportunity of gaining programming experience. You can choose one or more from the following topics.
Implementation of a model-checker for pushdown multi-agent systems [1,2]. Pushdown multi-agent systems are a natural model of infinite-state multi-agent systems. We have propose variants of model-checking algorithms for pushdown multi-agent systems, which can be used to automatically verify correctness of multi-agent systems.
Implementation of algorithms for checking emptiness of omega-pushdown automata. Omega-pushdown automata are pushdown automata over infinite words and are used to model sequential programs. Model-chcking problems of sequential programs can be reduced to the emptiness problems of omega-pushdown automata. Implementing those algorithms are useful for analyzing sequential programs.
Implementation of algorithms for checking reachability problem of pushdown systems with transductions, and its application to the verfication of boolean programs with call-by-reference [5].
There is no available algorithms or solutions. You will investigate the following problems with us. To be honest, you have to study lots of additional techniques from papers and books which is a bit challenging for you. It is a good opportunity of gaining reseaching experience and very helpful to students who are planning to attend gradate school. We require you ambitious, with clear future plan, smart, cooperative, fond of learning, good English skills. These topic could result in papers.
Automated testcases generation for Rust programs. Designing testcases is labor-consuming. Many automated testcases generation techniques were proposed and implemented to improve software development. By leverage existing techniques such as symbolic execution, concolic execution and model-checking, we are going to propose techniques and develop tool for testcase generation of Rust programs.
Rust compiler Testing. In programming language level, Rust guarantees memory safety, thread safety, etc. However, programs writting in high-level programming languages are compiled into machine codes which runs on CPU. It is possible to introduce bugs by the compiler [3]. We will propose and implement approaches to automatically test Rust compiler.
Formal semantics and type rules of the Rust programming language. Rust is a systems programming language that runs blazingly fast, prevents almost all crashes (memory safety), and eliminates data races, hence could be Rust a a good alternative to C++ for system programs. Semantics is the field concerned with the rigorous mathematical study of the meaning of programming languages and is essential to formally understand and analyze Rust programs. We will investigate formal semantics of the Rust programming language to better understand what a Rust program is doing and to prove. Currently, we are formalizing syntax and semantics of the Rust programming language in K semantic framework [4]. Memory safety of Rust is guaranteed by rigorous type systems. However, it is unclear what kind of type rules are implemented and checked in Rust compiler, are these type rules correct? We are going to formalize type rules of Rust.
Side-channel leak detection. Embedded computing devices (e.g., SIM card) often leak information about the software code that they execute through power and heat dissipation or electromagnetic radiation, which has been used to deduce secret information such as passwords and cryptographic keys. The current practice of manually designing countermeasures to mitigate such attacks is labor intensive and error prone. We aim to develop new efficient techniques to detect side-channel leak and prove the absence of side-channel leaks.
Error detection and compilation of floating-point programs. The accuracy of the floating-point computation is critical to many safety-critical applications, but floating-point programs are prone to accuracy problems due to rounding and catastrophic cancellation. For instance, on February 25, 1991, due to the accumulated floating-point errors, a Patriot missile failed to track and intercept an incoming missile in the Gulf War, caused the loss of 28 soldiers and around 100 injuries. We arm to develop new techniques to detect inaccuracy, generate solutions to improve accuracy.
Adversarial machine learning. Machine/deep learning techniques are widely used in security field such as malware detection, spam filtering and phishing website detection. We will propose new techniques for devising appropriate attacks that correspond to the identified threats and evaluating their impact on the targeted system, proposing countermeasures to improve the security of machine learning algorithms against the considered attacks.
Model checker for multi-agent systems. We aim to develop efficient model checking tools for automated verification of multi-agent systems, and its application to cooperative games, distribute protocols and agent-oriented programs.
References:
[1] Taolue Chen, Fu Song(Co-corresponding author) and Zhilin Wu. Verifying Pushdown Multi-Agent Systems against Strategy Logics. In Proc. of the 25th International Joint Conference on Artifficial Intelligence (IJCAI 2016). New York, USA. 9-15 July, 2016.
[2] Taolue Chen, Fu Song(Co-corresponding author) and Zhilin Wu. Global Model Checking on Pushdown Multi-Agent Systems. In Proc. of the 30th AAAI Conference on Artifficial Intelligence (AAAI 2016). Arizona, USA. 12-17 February, 2016.
[3] Junjie Chen, Wenxiang Hu, Dan Hao, Yingfei Xiong, Hongyu Zhang, Lu Zhang and Bing Xie. An Empirical Comparison of Compiler Testing Techniques. ICSE’16: 38th International Conference on Software Engineering, May 2016.
[4] http://www.kframework.org.
[5] On Reachability Analysis of Pushdown Systems with Transductions: Application to Boolean Programs with Call-by-Reference. Fu Song, Weikai Miao, Geguang Pu and Min Zhang. Proceedings of the 26th International Conference on Concurrency Theory (CONCUR 2015). Madrid, Spain. 1-4 September, 2015