| 2014 | TASE | Application-Specific Architecture Selection for Embedded Systems via Schedulability Analysis. | Han Liu, Hehua Zhang, Yu Jiang, Xiaoyu Song, Ming Gu, Jiaguang Sun |
| 2014 | TASE | iDola: Bridge Modeling to Verification and Implementation of Interrupt-Driven Systems. | Han Liu, Hehua Zhang, Yu Jiang, Xiaoyu Song, Ming Gu, Jia-Guang Sun |
| 2013 | ASPDAC | Sequential dependency and reliability analysis of embedded systems. | Hehua Zhang, Yu Jiang, Xiaoyu Song, William N. N. Hung, Ming Gu, Jiaguang Sun |
| 2013 | COMPSAC | Verification and Implementation of the Protocol Standard in Train Control System. | Yu Jiang, Hehua Zhang, Xiaoyu Song, William N. N. Hung, Ming Gu, Jiaguang Sun |
| 2013 | SEKE | DOPROPC: a domain property pattern system helping to specify control system requirements (S). | Fan Wu, Hehua Zhang, Ming Gu |
| 2011 | ICFEM | Domain-Driven Probabilistic Analysis of Programmable Logic Controllers. | Hehua Zhang, Yu Jiang, William N. N. Hung, Xiaoyu Song, Ming Gu |
| 2011 | TASE | Proving Computational Geometry Algorithms in TLA+2. | Hui Kong, Hehua Zhang, Xiaoyu Song, Ming Gu, Jiaguang Sun |
| 2010 | COMPSAC | Specifying Time-Sensitive Systems with TLA+. | Hehua Zhang, Ming Gu, Xiaoyu Song |
| 2009 | TASE | Specifying and Verifying PLC Systems with TLA+. | Hehua Zhang, Stephan Merz, Ming Gu |