Yucong Duan: Efficiency from Formalization: An Initial Case Study on Archi3D. SERA (selected papers) 2009: 1-12