X-IronPort-MID: 165915398
X-SBRS: 3.5
X-BrightmailFiltered: true
X-Ironport-AV: i="3.84,135,1091422800"; 
   d="scan'208"; a="165915398:sNHT12476840"
Content-Type: text/plain; charset=us-ascii
Date: Tue, 7 Sep 2004 01:04:01 -0500
From: hbl@cs.utexas.edu
To: acl2-mtg <acl2-mtg@lists.cc.utexas.edu>
Subject: Wednesday ACL2 Seminar: Java Program Verification 
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=-2.6 required=5.0
X-UTCS-Spam-Status: No, hits=-232 required=180

Hi, all, 

  This Wednesday, I will present my work on modeling the JVM
  and proving properties of simple Java programs via the JVM
  model. This opportunity will also get me better prepared
  for a similar presentation at TPHOLS 2004.

  I plan to start with some brief summary of computer-aid
  verification, ACL2, and my ongoing works. Then I will
  present a proof of "factorial" (again) on the current JVM
  model. I plan to show you the current JVM model. I will
  comment on our approach of Java program
  verification. Basically I plan to comment on the choice of
  "deep embedding" as opposed to "shallow embedding" in this
  type of work. I will also present the strategies and
  difficulties in proving properties of program executions
  on the complicated JVM model.

  I expect the talk will not be longer than 1 hour. 

hanbing


P.S. 
  http://coldice.csres.utexas.edu/~hbl/tphol2004/ has the
  paper that I will present at the TPHOLS conference. It is
  only an OK paper. In particular, the results are nothing
  exciting: a proof about ADD1 program, and another proof
  about a factorial program.