LARA This is an old revision of the document! This project consists in finding and implementing a mapping that permits generation of Alloy models from Jahob's datatype. The goal is to construct a bug finder based on SAT by coupling Alloy to Jahob.