Date: Tue, 1 Jun 2004 15:29:11 -0500 (CDT) From: "Jared C. Davis" Subject: ACL2 Meeting Tomorrow (June 2) Hi, We will have an ACL2 meeting tomorrow afternoon at 4:00. Fares Fraij will be presenting his work on modelling program transformations in ACL2. Fares writes: "The Sandia Secure Processor (SSP) is a project under development at Sandia National Labs. In this processor, a subset of the Java Virtual Machine (JVM) has been implemented in Hardware. Binary programs for the SSP ("Rom Images") are created from Java Class Files using an application program called the Class Loader, which is implemented using program transformations using the High-Assurance Transformation System (HATS). Its implementation consists of five phases, each using a set of transformation rules to accomplish a particular task." "I will be talking about the verification of the transformation rules that embody an abstraction of the first two phases of the class loader." Hope to see you there, Jared