Research Assistant Positions at Different Levels Available
I am currently looking for research assistants for the projects "Formal Modeling and Verification of Complex Concurrent Behavior in Cyber-Physical Systems" and "Trustworthy Deep Learning: Theories and Technologies" at postdoc/PhD level. The key criteria for the RA positions include good mathematical background and/or programming skills. The positions are available until the end of 2021 and applications for master students from international students are also welcome.
Undergraduate students from mathematics, computer science, information science or other related disciplines are also welcome to join my group for internship of research. Please feel free to contact me.
However, In the past years I have received many requests for (2-months or less) summer internships from undergraduate students (both from other universities in China and from other countries like India, Pakistan, etc,). However, due to administrative reasons I will not have such summer internships for students (I am usually out of the campus in July and August for conference trips and academic visits). If you just want to get a short summer research experience, please contact other professors.
Dr. Han Liu Visited Our Group
Dr. Han Liu from Blockhouse Technology Ltd. visited our group on Dec. 24, 2020, and gave a talk "Security Challenges and Analysis Technologies for Blockchain".
Invited talk at Beijing-Saint Petersburg Mathematics Colloquium
Meng Sun was invited to give a talk "Modeling and Verification of Concurrent and Distributed Systems: From Reo to Mediator" at Beijing-Saint Petersburg Mathematics Colloquium (online), December 3, 2020. Details could be found here.
ChinaSoft 2020 at Chongqing, China
The 2020 CCF ChinaSoft Conference (ChinaSoft 2020) was held at Chongqing, China from November 20 to 22, 2020. Xiyue Zhang was invited to give a talk: "Towards a formally verified EVM in production environment" at the YR-FMAC track, and participated in the Excellent PhD Candidate Forum. The Formal Methods Teaching Forum organized by Prof. Ji Wang and Meng Sun got the Excellent Forum Award at the conference.
Details of the conference can be found here.
CSIAM 2020 at Changsha, China
The 18th Annual Conference of China Society for Industrial and Applied Mathematics (CSIAM 2020) was held at Changsha, China from October 29 to November 1, 2020. Two students from our group gave talks at the conference: "Modeling and Verification of CKB Consensus Protocol against Selfish Mining Attacks" by Yuteng Lu at the session "Challenges on Blockchains Theories, Technologies and Applications" and "Modeling and Verification of the CKB Block Synchronization Protocol in Coq" by Hao Bu at the session "Computer Algebra and Information Security".
The programme of the conference can be found here.
Invited talk at NUDT, Changsha
Meng Sun was invited to give a talk "Modeling and Verification of Concurrent and Distributed Systems: From Reo to Mediator" at NUDT, Changsha, October 30, 2020.
Invited talk at Huawei ICT Software Technology Conference
Meng Sun was invited to give a talk "What Could We Do with Mathematics for Complex Software Systems?" at the 1st Huawei ICT Software Technology Conference, Xi'an, October 16-17, 2020.
Invited talk at FROM 2020
Meng Sun was invited to give a talk "Modeling and Verification of Concurrent and Distributed Systems in Mediator" at the 4th Working Formal Methods Symposium, Babes-Bolyai University, Romania, September 4-6, 2020. Details could be found here.
Wiseco FinTech Public Course on Formal Verification of Blockchain
Meng Sun was invited to give a lecture "Towards Safe FinTech: When Blockchain Meets Formal Verification" for the Wiseco Fintech public course series on August 27, 2020. Details could be found here.
BlockSys 2020
The paper "Modeling and Verification of the Nervos CKB Block Synchronization Protocol in UPPAAL" by Qi Zhang, Yuteng Lu and Meng Sun was accepted by BlockSys 2020. The conference was held online on August 6-7, 2020 and Qi Zhang gave the talk at the conference. Details about the conference could be found here.
ICSE 2020
The paper "Characterizing Adversarial Defects of Deep Learning Software from the Lens of Uncertainty" by Xiyue Zhang, Xiaofei Xie, Lei Ma, Xiaoning Du, Qiang Hu, Yang Liu, Jianjun Zhao and Meng Sun was accepted by ICSE 2020. The conference was held at Seoul (online) on June 24-July 16, 2020. The talk given by Xiyue Zhang at the conference is available at Youtube. Details about the conference could be found here.
Coordination 2020
The paper "Towards a Formally Verified EVM in Production Environment" by Xiyue Zhang, Yi Li and Meng Sun was accepted by Coordination 2020. The conference was held online on June 15-19, 2020. The talk given by Xiyue Zhang at the conference is available at Youtube. Details about the conference could be found here.
Congratulations to Ai Liu!
The PhD student Ai Liu has defended his theis successfully on June 10, 2020. Congratulations!
Prof. Marcello Bonsangue Visited Our Group
Prof. Marcello Bonsangue from Leiden University, the Netherlands, visited our group and gave a talk "On the Very Nature of Symbolic Execution" on November 22, 2019.
Hui Feng Visited Our Group
Hui Feng from Leiden University, the Netherlands, visited our group and gave a talk "A Reo Model of Software Defined Networks" on November 20, 2019.
Invited Talk at Capital Normal University
Meng Sun visited Information Engineering College at Capital Normal University, and gave a talk "Modeling and Verifying Complex Interactions in Concurrent Systems" on November 19, 2019.
Details of the talk can be found here.
Prof. Hongfei Fu Visited Our Group
Prof. Hongfei Fu from SJTU visited our group and gave a talk "Formal Verification of Probabilistic Programs: Termination, Cost Analysis and Sensitivity" at PKU on October 30, 2019.
ICFEM 2019 at Shenzhen, China
The 21st International Conference on Formal Engineering Methods (ICFEM 2019) was held at Shenzhen, China from November 5 to 9, 2019. The paper "A Coalgebraic Semantic Framework for Quantum Systems" by Ai Liu and Meng Sun, was presented at the conference.
The programme of the conference can be found here.
AI & FM 2019 at Shenzhen, China
The International Workshop on Artificial Intelligence and Formal Methods (AI & FM 2019) was held at Shenzhen, China on November 5, 2019. Meng Sun was invited to give a talk "Using RNN to Predict Tactics for Theorem Proving" at the workshop.
The programme of the conference can be found here.
Computing & AI Workshop 2019 at Shanghai, China
The workshop on Computing and Artificial Intelligence was held at Shanghai, China on September 23, 2019. Meng Sun was invited to give a talk "Using RNN to Predict Tactics for Theorem Proving" at the workshop.
CSIAM 2019 at Foshan, China
The 17th Annual Conference of China Society for Industrial and Applied Mathematics (CSIAM 2019) was held at Foshan, China from September 19 to 22, 2019. Meng Sun was invited to give a talk "Towards A Formally Verified EVM in Production Environment" at the session "Challenges on Mathematical Theories, Technologies and Applications for Blockchains".
The programme of the conference can be found here.
Lingtai Wang Visited Our Group
Lingtai Wang from ISCAS visited our group and gave a talk "The Opacity of Real-time Automata" on September 18.
Dr. Bai Xue Visited Our Group
Dr. Bai Xue from ISCAS visited our group and gave a talk "Safe Inputs Generation for Black-box Systems" on September 11.
TASE 2019 at Guilin, China
The 13th International Symposium on Theoretical Aspects of Software Engineering (TASE 2019) will be held at Guilin, China from July 29 to August 1, 2019. Two papers "Distributed Mediator" by Yi Li and Meng Sun, and "Using Recurrent Neural Network to Predict Tactics for Proving Component Connector Properties in Coq" by Xiyue Zhang, Yi Li, Weijiang Hong and Meng Sun were presented at the symposium.
The programme of the symposium can be found here.
Prof. Fu Song Visited Our Group
Prof. Fu Song from ShanghaiTech University visited our group and gave a talk "程序侧信道安全形式化验证" on July 25.
SEKE 2019 at Lisbon, Portugal
The 31st International Conference on Software Engineering & Knowledge Engineering (SEKE 2019) will be held at Lisbon, Portugal from July 10 to 12, 2019. The paper "PRISM Code Generation for Verification of Mediator Models" by Weidi Sun and Meng Sun, was accepted by the conference.
The programme of the conference can be found here.
Dr. Guangdong Bai Visited Our Group
Dr. Guangdong Bai from Griffith University visited our group and gave a talk "Trusted Computing based Protocols: Modeling and Analysis" on July 4.
SERVICES 2019 at San Diego, USA
The 2019 World Congress on Services (SERVICES 2019) will be held at San Diego, USA from June 25 to June 30, 2019, which is co-located with 9 other service-oriented conferences, such as ICWS, CLOUD, ICIOT, ICBC, etc. The paper "SMT-based Modeling and Verification of Cloud Applications" by Xiyue Zhang and Meng Sun, was accepted by SERVICES 2019.
The programme of the conference can be found here.
Congratulations to Yi Li, Saqib Nawaz, Heyuan Xu, Shun Wang and Yuanyi Ji!
The PhD students Yi Li, Saqib Nawaz, and master students Heyuan Xu, Shun Wang and Yuanyi Ji have defended their theis successfully. Congratulations to them all!
Dr. Yu Guo Visited Our Group
Dr. Yu Guo from SECBIT Labs visited our group and gave a talk "Blockchain based protocols for fair trading" on May 30, 2019.
Details of the talk can be found here.
Xiaohong Chen Visited Our Group
Mr. Xiaohong Chen from UIUC visited our group and gave a talk "Matching mu-logic: A powerful logic for specifying and reasoning about fixpoints and induction, programming languages, and program specification and verification" on May 23, 2019.
Details of the talk can be found here.
FSEN 2019 at Tehran, Iran
The 8th IPM International Conference on Fundamentals of Software Engineering (FSEN 2019) was held at Tehran, Iran from May 1 to May 3, 2019. The PhD student in our group, M. Saqib Nawaz, gave two talks "Proof Guidance in PVS with Sequential Pattern Mining" and "Using PVS for Modeling and Verification of Probabilistic Connectors" at the conference.
The programme of the conference can be found here.
Prof. Grigore Rosu Visited Our Group
Prof. Grigore Rosu from UIUC visited our group on April 18-20, 2019 and gave a talk "Formal Design, Implementation and Verification of Blockchain Languages". Details of the talk can be found here.
2019 Seminar
The group seminar in 2019 spring will be held every Thursday, 09:00-11:00.
Details about the seminar schedule can be found here.