panagiotis manolios tzixnsdvccgatechedu call participation acl2 2006 international workshop acl2 theorem prover applications incooperation acm sigplan acm sigsoft httpwwwccgatechedumanoliosacl206 august 1516 2006 seattle washington part floc 2006 httpresearchmicrosoftcomfloc06 hosted cav 2006 ijcar 2006 early registration deadline july 10 2006 regular registration deadline august 1 2006 hotel registraion deadline july 21 2006 acl2 2006 major technical forum users acl2 theorem proving system sixth series workshops occur every 18 months acl2 industrialstrength automated reasoning system part boyermoore family theorem provers winner 2005 acm software system award invited talk tony hoare microsoft research ideal verified software panel david hardin tony hoare gerard holzmann j strother moore grand challenge problems acl2 community program tuesday august 15 850900 pete manolios matt wilding welcome opening remarks session 1 900930 lee pike mark shields john matthews verifying core cryptographic language compiler 9301000 david hardin eric smith william young robust machine code proof framework highly secure applications 10001030 break session 2 10301100 john cowles ruben gamboa unique factorization acl2 part 1 euclidean domains 11001130 david greve parameterized congruences acl2 11301145 sol swords william cook soundness simply typed lambda calculus acl2 11451230 matt kaufmann j strother moore overview recent upcoming acl2 developments 12301400 lunch break session 3 14001430 erik reeber warren hunt jr satbased procedure verifying finite state machines acl2 14301500 julien schmaltz dominique borrione towards formal theory chip communications acl2 logic 15001515 jared davis memories arraylike records acl2 15151530 acm software system award session 15301600 break session 4 16001645 invited speaker tony hoare ideal verified software 16451815 david hardin tony hoare gerard holzmann j strother moore panel grand challenge problems acl2 community 19002130 workshop dinner wednesday august 16 session 5 900930 erik reeber jun sawada combining acl2 automated verification tool verify multiplier 9301000 ruben gamboa john cowles implementing costaware evaluator acl2 expressions 10001030 robert boyer warren hunt jr function memoization unique object representation acl2 functions 10301100 break session 6 11001115 david l rager adding parallelization capabilities acl2 11151130 sandip ray quantification tailrecursive function definitions 11301145 warren hunt jr serita nelesen phylogenetic trees acl2 11451200 matt kaufmann j strother moore double rewriting equivalential reasoning acl2 12001230 tba rump session 12301400 lunch break session 7 14001430 dale vaillancourt rex page matthias felleisen acl2 drscheme 14301500 jared davis reasoning acl2 file input 15001530 mike gordon warren hunt jr matt kaufmann james reynolds embedding acl2 logic hol 15301600 break session 8 16001745 matt kaufmann j strother moore discussion possible future enhancements acl2 16451730 pete manolios matt wilding business meeting organization chairs panagiotis manolios georgia institute technology matthew wilding rockwell collins inc publications ruben gamboa university wyoming webmasters sudarshan srinivasan georgia tech daron vroon georgia tech program committee ruben gamboa university wyoming usa david greve rockwell collins inc usa warren hunt university texas austin usa deepak kapur university new mexico usa matt kaufmann university texas austin usa bill legato nsa usa panagiotis manolios georgia institute technology usa jose meseguer university illinois urbanachampaign usa paul miner nasa langley research center usa j strother moore university texas austin usa lawrence c paulson university cambridge uk jose luis ruizreina university seville spain david russinoff advanced micro devices inc usa jun sawada ibm austin research laboratory usa mary sheeran chalmers university technology sweden konrad slind university utah usa matthew wilding rockwell collins inc usa thu 07 aug 2008 032232 0400 uai acl2 2006 call participation