X-IronPort-MID: 824371721 X-SBRS: 3.7 X-BrightmailFiltered: true X-Brightmail-Tracker: AAAAAA== X-Ironport-AV: i="3.92,128,1112590800"; d="scan'208"; a="824371721:sNHT13327472" Date: Mon, 25 Apr 2005 14:32:36 -0500 From: Jared Davis User-Agent: Debian Thunderbird 1.0 (X11/20050116) X-Accept-Language: en-us, en To: ACL2 MTG List Subject: This week in ACL2 Content-Type: text/plain; charset=ISO-8859-1; format=flowed 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, At this week's ACL2 meeting, Hanbing Liu will be discussing Abstract Interpretation. He writes: "Abstract interpretation is a unified way for studying the justification for existing program analysis techniques, including: 1. Static analysis conducted by compiler for optimization; 2. Bytecode verification for confirming actual execution safety; 3. Modeling checking for safety and liveness; In the first part of the talk, I expect to follow the beginning part of the paper by David A. Schmidt: "Abstract Interpretation in the Operational Semantics Hierachy" I will give a simple presentation of the intuitive concepts. Later in the talk, I plan to cast my work for verifying the bytecode verifier in terms of abstract interpretation. For a more rigorous treatment, I recommend Cousot's original paper (Just google the title you will find it): "Abstract Interpretation: A Unified Lattice Model For Static Analysis of Programs by Construction or Approximation of Fixpoints" However, this paper only covers the abstract interpretation of flowchart programs." Hope to see you there, Jared -- Jared Davis http://www.cs.utexas.edu/users/jared/ 1003 Justin Lane #1008 - Austin TX 78757 Home 512-374-9474; Office 512-471-9744