X-IronPort-MID: 110046817 X-SBRS: 5.5 X-BrightmailFiltered: true X-Brightmail-Tracker: AAAAAQAAA+k= X-IronPort-AV: i="4.02,135,1139205600"; d="scan'208"; a="110046817:sNHT16802128" Date: Tue, 21 Feb 2006 17:16:11 -0600 (CST) From: Sandip Ray To: acl2-mtg@lists.cc.utexas.edu Subject: This week in ACL2 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=-212 required=180 Greetings, At the ACL2 meeting this week, I will talk about ongoing work on the integration of assertional reasoning with operational semantics using ACL2. Here is the title and abstract for the talk. Hope to see you there. --- Sandip. TITLE: Assertional Reasoning Using Symbolic Simulation: The Ingredients Abstract: Recently there has been a lot of interest in the ACL2 community to apply assertional reasoning to verify sequential programs executed on machines that are formally modeled using operational semantics. The research starts from a key observation by J Moore in 2003, and has since been extended by several people, including J Moore, John Matthews, Daron Vroon, me, and Eric Smith. In this talk I will give a brief overview of the goals of this work, and discuss some key ingredients in the ACL2 logic that make it possible. The most important ingredient is our ability to axiomatize tail-recursive "partial" functions using quantification and Skolemization. and I will discuss how such functions are specified and how they enable us to do assertional reasoning using symbolic simulation. I hope to touch on the basic elements of the work, but if time permits we will look at how we can automate many of the generic results using macros and functional instantiation, and what issues are involved in such automation.