Control Synthesis for a Smart Card Personalization System Using Symbolic Model Checking. - Biniam Gebremichael; Frits W. Vaandrager (FORMATS, 2003)

Deadlock Prevention in the Æthereal Protocol. - Biniam Gebremichael; Frits W. Vaandrager; Miaomiao Zhang; Kees Goossens; Edwin Rijpkema; Andrei Radulescu (CHARME, 2005)

The Coarsest Congruence for Timed Automata with Deadlines Contained in Bisimulation. - Pedro R. D'Argenio; Biniam Gebremichael (CONCUR, 2005)

Specifying Urgency in Timed I/O Automata. - Biniam Gebremichael; Frits W. Vaandrager (SEFM, 2005)

Analysis of the zeroconf protocol using UPPAAL. - Biniam Gebremichael; Frits W. Vaandrager; Miaomiao Zhang (EMSOFT, 2006)

Formal specification and analysis of zeroconf using uppaalS. - Jasper Berendsen; Biniam Gebremichael; Frits W. Vaandrager; Miaomiao Zhang (ACM Trans. Embed. Comput. Syst., 2011)