Shilov N., Bodin E., Shilova S. Guided tour inside F@BOOL@: a case-study for a SAT-based verifying compiler // Computer Science. — 2010. — # 31 — P. 139-154
Shilov N., Bodin E., Shilova S. Fabulous arrays I: Operational and transformational semantics of static arrays in verification project F@BOOL@ // Computer Science. — 2009. — # 29 — P. 119-138