A preliminary report on xMECH

Abstract

This document reports the current development status of xMECH. It is an implementation of the so-called skin or hybrid embedding approach [1] for HOL. Its purpose is to enhance HOL's power and interaction to do software verification. xMECH features languages and logics to describe and verify sequential and distributed programs, a reasonably rich expression language to write specifications, and optimized verification condition generators. It is available for public use, but it is still in a prototype phase, with limited features and user support. It comes with some simple demos, but doing a serious project with xMECH is not (yet) recommended for an inexperienced user.