Shaowei Cai is a Professor at Institute of Software, Chinese Academy of Sciences, leader of the Constraint Solving group. He received his PhD degree from Peking University with Distinguished Doctoral Dissertation Award. His research interests include constraint solving and formal methods. Particularly, he has regularly won Gold/Silver medals in recent SAT Competitions, including 5 Gold medals in Parallel tracks won by the PRS solver in his team. The SMT solvers Z3++ and Parti-Z3++ has won “largest contribution” award and “largest leading” awards in Model Validation track and Cloud track in SMT Competitions. He has received the Best/Distinguished Paper Award at SAT 2021, CP 2024 and CAV 2024. He has given tutorials at FMCAD and SoCS conferences.

Samarjit Chakraborty is a Kenan Distinguished Professor of Computer Science at UNC Chapel Hill. He is also an adjunct professor of Mathematics at UNC. Prior to coming here, he was a professor of Electrical Engineering at the Technical University of Munich in Germany, where he held the Chair of Real-Time Computer Systems for 11 years. Before that he was an assistant professor of Computer Science at the National University of Singapore. He obtained his PhD from ETH Zurich. His research interests cover all aspects of designing hardware and software for embedded computers, with an emphasis on cyber-physical systems design, sustainable computing, and sensor network-based information processing. He serves/d on the editorial boards of several journals, including the ACM Transactions on Cyber-Physical Systems and the ACM Journal on Autonomous Transportation Systems. He and his students have won several best paper awards for their work, including the 2019 ACM Transactions on Design Automation of Electronic Systems Best Paper Award for their work on automotive security, and the 2021 ACM Transactions on Embedded Computing Systems Best Paper Award for their work on energy modeling of the Bluetooth Low Energy protocol. He is a Fellow of the IEEE and was offered a Humboldt Professorship from Germany in 2023.

Kim Guldstrand Larsen is Professor in Computer Science at Aalborg University, Denmark. His field of research includes modeling, validation and verification, performance analysis, and synthesing of real-time, embedded, and cyber-physical systems utilizing and contributing to concurrency theory, model checking and model checking. Kim Guldstrand Larsen is co-founder and main contributor to the tool UPPAAL. UPPAAL received the prestigious CAV Award in 2013 as the foremost tool for modelling and verification of real-time systems. Kim Guldstrand Larsen won the ERC Advanced Grant in 2015 and won a Villum Investigator grant in 2021. In 2022 he received the CONCUR Test-of-Time Award 2022.

Kim Guldstrand Larsen is a member of Royal Danish Academy of Sciences and Letters, elected fellow and digital expert (vismand) in the Danish Academy of Technical Sciences and Knight of the Order of the Dannebrog (2007). Moreover he is Honorary Doctor, Uppsala University (1999), Honorary Doctor, École normale supérieure Paris-Saclay, Paris (2007), Foreign Expert of China, Distinguished Professor, Northeastern University (2018). He has published more nearly 500 peer-reviewed papers and received Thomson Scientific Award as the most cited Danish computer scientist 1990-2004.

Jan Reineke is a professor of computer science at Saarland University. Before joining Saarland University in 2012, he has been a postdoctoral scholar at UC Berkeley in the Ptolemy group from 2009 to 2011. He completed his MSc and PhD in Computer Science at Saarland University in 2005 and 2008, respectively, and his BSc in Computing Science at the University of Oldenburg in 2003.

His research centers around problems at the boundary between hardware and software.

In the area of real-time systems, he is particularly interested in principles for the design of timing-predictable hardware and in precise and efficient timing-analysis techniques for multi-core architectures. His recent results include the design of the first provably timing-predictable pipelined processor design (RTSS 2018) and the first exact analyses for LRU caches (CAV 2017, POPL 2019, RTSS 2019).

Another focus of his work are security vulnerabilities of hardware-software systems. Recent results include the development of automatic techniques to detect information leaks introduced by speculative execution (Spectector, S&P 2020), techniques to quantify the information leakage through cache side channels (ACM TISSEC 2015), and automatic methods to obtain highly detailed performance models for modern microarchitectures (uops.info, ASPLOS 2019).

In 2012, he was selected as an Intel Early Career Faculty Honor Program awardee. He was the PC chair of EMSOFT 2014, the International Conference on Embedded Software, a Topic co-chair at DATE 2016 and the PC chair of WCET 2017, the International Workshop on Worst-Case Execution Time Analysis. His papers have been awarded 9 outstanding paper awards and two best-paper nominations, most recently at DATE (2024), CCS (2023), RTSS (2023, 2019, 2018), Oakland (2021), and ECRTS (2017). In 2021, he has been awarded an ERC Advanced Grant.

Pedro Ribeiro is a Lecturer (Assistant Professor) in Computer Science at the University of York, UK. Previously, he was a Research Fellow in the School of Physics Engineering and Technology at York, and before that a Research Associate in Computer Science. He completed his PhD at York on the treatment of angelic nondeterminism for process calculi. He has over a decade of experience with formal approaches to software engineering relevant to robotics and cyber-physical systems more generally. His research interests span the breadth of the engineering lifecycle, spanning from design and development of domain-specific notations and their semantics, to testing and formal reasoning using automated mathematical proof techniques. He is a member of the York’s RoboStar centre for Excellence in Software Engineering for Robotics, and a founding member of Formal Methods Europe’s communications committee.

Xue Yinxing is currently a Research Professor at the Institute of Artificial Intelligence for Industries, specializing in software security. He received his Ph.D. from the National University of Singapore (NUS) and subsequently conducted defense-related research at the Temasek Laboratories of National University of Singapore and Nanyang Technological University in Singapore. In 2018, he was recruited through the CAS Talent Program to join the University of Science and Technology of China (USTC). He has led 6 national and provincial/ministerial-level research projects. Notably, he has spearheaded two international standards for intelligent connected vehicles (ICVs) at ISO/ITU, with one ITU standard and one IEEE standard successfully being approved and under development. His recent academic achievements include: 24 first/corresponding-author publications in the past six years (19 in CCF Rank A venues), two-time recipient of the ACM SIGSOFT Distinguished Paper Award.

Min Zhang is a full professor at the Software Engineering Institute, East China Normal University. He earned his Ph.D. from the Japan Advanced Institute of Science and Technology in 2011 and joined East China Normal University in 2014. From 2019 to 2021, he served as a senior visiting professor at Nice University. His research interests primarily focus on formal methods for safety-critical systems, including real-time and AI-empowered systems. Recently, he has concentrated on the formal verification of deep neural networks and intelligent systems. He has co-authored over 80 papers, published in top-tier conferences such as CAV, TACAS, ASE, ICSE, NeurIPS, CVPR.

Dr. Ji Guan is currently an Associate Research Professor at the Institute of Software, Chinese Academy of Sciences (CAS). His main research interests are formal methods for quantum computing, focusing on systematically addressing the security, privacy, and reliability of quantum systems by developing formal method (verification) theories, algorithms, and tools. He has published nearly 20 papers in top international conferences and journals in the field, such as CAV, FM, IEEE TIT, ACM CCS, and SICOMP. He was selected for the 10th Young Elite Scientists Sponsorship Program by the China Association for Science and Technology. He is a member of the Youth Innovation Promotion Association of CAS and a recipient of the Beijing High-level Overseas Talents Funding Program (top 30). In addition, he serves as a program committee member for several leading international conferences, including CAV and QCNC.

Fei He is a tenured Associate Professor in the School of Software at Tsinghua University. His research interests include program verification, model checking, and automated logical reasoning. He has published over 90 papers in academic journals and international conferences. He currently serves on the editorial board of Theory of Computing Systems and has served on the program committees of numerous international conferences, including OOPSLA, ICSE, ESEC/FSE, CONCUR, FMCAD, SAT, etc.

Wang Lin is currently a professor with Zhejiang Sci-Tech University. His research interests include verification and design of cyber-physical systems. Many of his works were published in top-tier conferences and journals on AI and formal methods, e.g., TCAD, TECS, CAV, FM, EMSOFT, HSCC, CVPR, AAAI, IJCAI.

Meng Sun received his BS degree in Information Science and PhD degree in applied mathematics from Peking University in 1999 and 2005, respectively. He worked as a postdoc researcher at National University of Singapore from 2005 to 2006, and as a scientific staff member at CWI, the Netherlands, from 2006 to 2010. He joined Peking University in 2010 and currently is a full professor at School of Mathematical Sciences in Peking University. His research interests mainly lie in theories of programming, software formal methods, cyber-physical systems, trustworthiness guarantee of AI systems, blockchain and smart contracts. His publications appear in top-tier venues including TSE, TDSC, ICSE, FSE, FM, NeurIPS and AAAI. He has served as PC Co-chair of ICFEM (2024 and 2018), TASE (2023), FACS (2024 and 2009), and PC member of international conferences such as FM and TACAS.

Yingfei Xiong obtained his Ph.D. degree from the University of Tokyo in 2009, and worked as a postdoctoral researcher at University of Waterloo from 2009 to 2011. He joined Peking University in 2012 and is currently a tenured associate professor, deputy director of the Institute of Software. His research interest is programming languages and software engineering in general, and program synthesis, repair, analysis and verification in particular. His work has contributed to the development of a series of neural network models for code generation that achieve state-of-the-art performance across different scales, such as the DeepSeek-Coder model; significantly improved the precision, recall, and efficiency of program repair; proposed delta-based BX, one of the two most widely used bidirectional transformation frameworks; successfully solved numerous algorithm design problems, including those from world-class competitive programming contests. His work has been adopted by industry, such as by Huawei, ZTE, and the next-generation Linux kernel configuration project. He has served as the vice chair of OOPSLA, area chair of ASE, and editorial board member of IEEE TSE. He regularly serves on the program committees (PC) of conferences like PLDI, ICSE, FSE, OOPSLA, ASE, and ISSTA, and has received five Distinguished Reviewer Awards at ICSE and FSE. He was awarded the First Prize of the National Technology Invention Award (6th recipient), the First Prize of the Chinese Institute of Electronics Natural Science Award (ranked 1st), the CCF-IEEE CS Young Scientist Award, the MODELS Ten-Year Most Influential Paper Award, and five ACM SIGSOFT/IEEE TCSE Distinguished Paper Awards. He is a Distinguished Member of ACM and a member of IFIP WG 2.4.

Bai Xue a professor at the Key Laboratory of System Software (Chinese Academy of Sciences), Chinese Academy of Sciences (formerly known as the State Key Laboratory of Computer Science at the Institute of Software, CAS) since September 2021. In September 2024, he was appointed Deputy Director of the Key Laboratory of System Software. His research interests mainly involve, but are not limited to, verification and control of cyber-physical systems, safe reinforcement learning, and control theory.

He received the B.Sc. degree in information and computing science from Tianjin University of Technology and Education in 2008, and the Ph.D. degree in applied mathematics from Beihang University in 2014. Prior to joining Institute of Software as an associate research professor in November 2017, he worked as a research fellow in the Centre for High Performance Embedded Systems at Nanyang Technological University from May, 2014 to September, 2015, and as a postdoc in the Department für Informatik at Carl von Ossietzky Universität Oldenburg from November, 2015 to October, 2017.

Song Yan studied both Mathematics and Computer Science, and obtained a PhD in Mathematics (Number Theory) from University of York, UK. He has been working in UK/US universities for over 30 years and published 6 research monographs at Springer; some of them has been translated into Russian, Polish and Chinese. His has a wide range of research interests in number theory, computing theory, quantum computing, cryptography, cyber security, and AI/machine learning.