Recently, the research achievement “Computing Semi-Algebraic Invariants for Polynomial Dynamical Systems,” with Liu Jiang of our institute as the first author, won the EMSOFT Test of Time Award at the 2026 IEEE/ACM International Conference on Embedded Software.
EMSOFT is one of the three core conferences of IEEE/ACM Embedded Systems Week (ESWEEK), has been the premier venue for cutting-edge research in the design and analysis of software that interacts with physical processes, with a long-standing tradition for results on cyber-physical systems, which compose computation, networking, and physical dynamics. Since 2019, ESWeek has established the Test of Time Awards to honor the authors of CASES, CODES+ISSS and EMSOFT papers that have demonstrated to have had a major and lasting impact on their respective research fields. Among them, the EMSOFT Test of Time Award specifically recognizes papers published at EMSOFT that are at least 10 years old and have had a longstanding impact.
The award-winning paper was published at the 11th ACM International Conference on Embedded Software (EMSOFT 2011) held in Taipei, China. All three authors of the paper are from the Chinese Academy of Sciences. The collaborators include Researcher Zhan Naijun from the Institute of Software, Chinese Academy of Sciences (now Boya Distinguished Professor at the School of Computer Science, Peking University) and Dr. Zhao Hengjun (now Associate Professor at the College of Computer and Information Science, Southwest University). This is the first time that the EMSOFT Test of Time Award has been awarded to a paper whose affiliated institutions are all in China and all of whose authors are Chinese scholars.
The paper focuses on the automatic discovery and verification of “semi-algebraic invariants” in polynomial dynamical systems (PDS). Dynamical systems are widespread in physical simulation, control engineering, and the actual processes described by embedded software; invariants characterize the “safety boundary” that a system will never cross during its evolution.
Figure 1. Concept of invariants
If such invariants can be automatically found and proved, rigorous mathematical guarantees can be provided for the reliability of safety-critical systems. The core contribution of the paper is as follows: it establishes a sound and relative complete decision criterion for semi-algebraic invariants for polynomial dynamical systems with domains and initial conditions, and thereby provides an invariant generation method based on template hypotheses and semi-algebraic constraint solving.
Figure 2. Main results
The “relative completeness” conclusion in the achievement means that as long as an invariant exists in a pre-specified template form, the method can compute it. The computation of semi-algebraic invariants directly determines whether it is possible to rigorously prove, in complex systems coupling continuous evolution and discrete jumps, that the system will never enter a dangerous state.
This work theoretically answers the fundamental question of “how to systematically determine and construct safe regions of polynomial dynamical systems,” and provides rigorous mathematical tools for the subsequent formal verification of nonlinear hybrid systems. It has laid a key theoretical foundation for the formal verification of safety-critical embedded and hybrid systems (such as autonomous driving, intelligent transportation, and medical monitoring devices). It has been extended by subsequent research to non-autonomous dynamical systems and hybrid systems with discrete transitions, and continues to promote China’s basic research in trustworthy embedded software and cyber-physical systems toward leading, original, and forward-looking development.