A note on "a mapping algorithm for computer-assisted exploration in the design of embedded systems". - Gang Chen 004; Xiaoyu Song; Feng Liu 029; QingPing Tan; Fei He 001 (ACM Trans. Design Autom. Electr. Syst., 2007)

Formalization and Verification of PLC Timers in Coq. - Hai Wan; Gang Chen 004; Xiaoyu Song; Ming Gu 001 (COMPSAC (1), 2009)

A Comparative Study of Parallel Prefix Adders in FPGA Implementation of EAC. - Feng Liu 029; Fariborz Fereydouni-Forouzandeh; Otmane Aït Mohamed; Gang Chen 004; Xiaoyu Song; QingPing Tan (DSD, 2009)

Formal Proof for a General Architecture of Hybrid Prefix/Carry-Select Adders. - Feng Liu 029; QingPing Tan; Xiaoyu Song; Gang Chen 004 (ICA3PP (1), 2010)

A Refinement-Based Validation Method for Programmable Logic Controllers. - Hai Wan; Xiaoyu Song; Gang Chen 004; Ming Gu 001 (QSIC, 2010)

Field programmable gate array prototyping of end-around carry parallel prefix tree architectures. - Feng Liu 029; Qingping Tan; Gang Chen 004; Xiaoyu Song; Otmane Aït Mohamed; Ming Gu 001 (IET Comput. Digit. Tech., 2010)

Formal proof of prefix adders. - Feng Liu 029; Qingping Tan; Gang Chen 004 (Math. Comput. Model., 2010)

Proofs of Correctness and Properties of Integer Adder Circuits. - Gang Chen 004; Feng Liu 029 (IEEE Trans. Computers, 2010)

Formal Analysis of End-Around-Carry Adder in Floating-Point Unit. - Feng Liu 029; Xiaoyu Song; Qingping Tan; Gang Chen 004 (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2010)

Formal Analysis of Hybrid Prefix/Carry-Select Arithmetic Systems. - Feng Liu 029; Xiaoyu Song; Qingping Tan; Gang Chen 004 (Comput. J., 2011)

Formalisation and verification of programmable logic controllers timers in Coq. - Hai Wan; Gang Chen 004; Xiaoyu Song; Ming Gu 001 (IET Softw., 2011)