X-IronPort-MID: 1805724755 X-SBRS: 4.2 X-BrightmailFiltered: true X-Brightmail-Tracker: AAAAAQAAA+k= X-IronPort-AV: i="4.02,169,1139205600"; d="scan'208"; a="1805724755:sNHT15391436" Date: Mon, 6 Mar 2006 17:29:27 -0600 From: hbl@cs.utexas.edu To: acl2-mtg Subject: ACL2 Seminar: Specify and Verify a Simple Virtual Machine Reply-To: acl2-mtg@lists.cc.utexas.edu Sender: owner-acl2-mtg@lists.cc.utexas.edu X-Listprocessor-Version: 8.2.10/020311/17:52 -- ListProc(tm) by CREN X-SpamAssassin-Status: No, hits=-1.6 required=5.0 X-UTCS-Spam-Status: No, hits=-112 required=180 Hi, I am going to talk at the ACL2 meeting this week. Here is the background and abstract of my talk. ----------------------------------------------------------- The official Java Virtual Machine specification (JVMSpec) describes a Platonic machine for executing the bytecode programs. The JVMSpec specifies the semantics of machine instructions -- however, only when the JVM state (for executing the instruction in) satisfies a set of declarative constraints. In other cases, the behavior of the JVM is undefined. The JVMSpec also describes an algorithmic bytecode verifier that is designed to detect "unsafe" programs --- programs that may induce the JVM into a state that violates the declarative constraints. (thus initiate undefined behaviors) The hope is that by refusing to execute the unsafe program, the declarative constraints are alway met --- consequently, behaviors of program executions are well defined. One interesting question is whether the algorithmic bytecode verification mechanism is "effective". In this talk, I specify a much simpler virtual machine --- in the same style of the JVMSpec: 1. incomplete specification of machine instruction semantics 2. a separate checker that designed to reject unsafe programs --- using the JVM bytecode verifier like algorithm. I discuss why the static checking algorithm works and present some top level approach for proving that with ACL2. I donot plan to present the ACL2 proof itself. I will present the goal theorem. ----------------------------------------------------------- hanbing