coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] ACL2-2025 Call for Participation

From: Matt Kaufmann <kaufmann AT cs.utexas.edu>
To: kaufmann AT cs.utexas.edu
Subject: [Coq-Club] ACL2-2025 Call for Participation
Date: Fri, 14 Mar 2025 09:26:38 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=kaufmann AT cs.utexas.edu; spf=Pass smtp.mailfrom=kaufmann AT cs.utexas.edu; spf=Pass smtp.helo=postmaster AT newman.cs.utexas.edu
Ironport-data: A9a23:lzeDlKngx2I0t+b7ukubTbzo5gwNIkRdPkR7XQ2eYbSJt1+Wr1Gzt xIeXjqCM/eMNDTwLYokYYzk9U8D7cSDm4dqSQVt/no8FVtH+JHPbTi7BhepbnnKdqUvb2o+s p5AMoGYRCwQZiWBzvt4GuG59RGQ7YnRGvymTrSs1hlZHWdMUD0mhQ9oh9k3i4tphcnRKw6Ws LsemeWGULOe82Ayaz58B56r8ks14ayp4W9A5zTSWNgS1LPgvylNZH4gDfrpR5fIatE8NvK3Q e/F0Ia48gvxl/v6Io7Nfh7TKyXmc5aKVeS8oiI+t5uK3nCukhcPPpMTb5LwX6v4ZwKhxLidw P0V3XC5pJxA0qfkwIzxWDEAe81y0DEvFBYq7hFTvOTKp3AqfUcAzN01HhlqFr80o9wvCGdez 60fdQ0QaAyc0rfeLLKTEoGAh+wlIdbuNYVZsWom0C3UHf89B53PXs0m5/cBhmd21psIRK2PI ZNAMVKDbzyYC/FLElQeFZw7leGurnLkNSBEpUKcvuw673W7IAlZiuG3YYGJI4zXLSlTtkyHu XDJ1kjjOCMlboGDyjWG+CzwguCayEsXX6pOS+Dnr5aGmma7zWsKTRYSSFGTuui8kkf4WtRFK kVS9DBGkEQp3EqmUdz0WVuzuziZohMMUsEWHuEngO2Q9kbKy12LXjQvfBIYUoQvst8MFDt36 0KPg8y8UFSDr4apYX6a876Vqxa7Ni4UMXIOaEc4oe0tvYOLTGYb00qnczpzLJNZmOEZDt0Z/ txnhC4zmLAai4gAzOOm4V3Xiinqq5TUJuLU2uk1dj/4hu+aTNf7D2BN1bQ9xawYRGp+ZgPR1 EXoY+DEsIgz4WilzURhutklErCz/OqiOzbBm1NpFJRJ323ypyfzLNgPuGoveB4B3iM4ldnBP he7VeR5uM47AZdWRfEfj3+ZUZpxlPawfTgbfqGKNYImjmdNmP+voH4zOhf4M5HFjU4tj6wlI paHYI6rAz4GBLRu13K/W68UzKQ3xyZW+I8gbcuT8vhT6pLHPCT9Ye5cYDOmMLplhJ5oVS2Mo 76zwePTm00HCIUTo0D/reYuELz9BSFjVM+n95QHL7brz8gPMDhJNsI9CIgJI+RN95m5XM+Sl p1kchYAkASttm6NMgiQdHFoZZXmWJs1/zpxPjUhMRzskzIvaJqmpvVXPZYmX6gVxMo6x95NT t4BZ5qhBNZLQW/54DgzV8T2g7FjUxWJvjiwGRSZTgIxRaM9eDyRyOTYJlPu0AIsEhuIsdAPp uz89wHDHrsGaQdQLOfXT/ONzVig4CERt9wubnvtP+tsQhzN8ZdrGQP1nPQYM8EBEjSd5zq4h iK9IwYUmvnJmKAxqOL2vKGjq5zzNflTBW9YIjX/wZOpExeC5Uul44tLcNjQTADnTGmupZmTP 7RE/c/zINgsvQhssbMlN51J0Khnxd/kh4EC/zReBH+RMmiaUOJxEEKng/tKmLZGnIJCmA2MX UmKxNlWFJOJNO7hE38TPAAVVfuC595Fhgjt6ekJH2ui6B9V5LanVWBgDyuIggFZL5p3N9oB6 sUls8g09Qe+q0QLNvCrsyNqzFmPf0cwC/gfipInAYHQmlUKzHNGasfiESPY2syEROhNFUgIG QWqopT+qY5S/Wf8VkYiNGPs2LNdjKseuRoRw14lIU+Iq+X/hfQ2/UNw9GkzQl4Mzh9GjuB4K zUyO2JLeZS+2ipau/IafmGzGjNuAA+S1VzxxmAoykzYbRiMfU7cIFItPd2i+BgizFtdWTxA7 pS09X3DUz36WO3QhwwcAVVErd7nRvxPrjzyotitRZm5LsNrcAjbjb+LTktWjRneWOcaplDN/ Mtu98ZOMZzLDzYa+fAHOtPLxIYraU62IUJZSqtc54IPJ2bXfQ+y1RWoK0ycfsBsJeTAwXSnC v5Bd95+aBCj6Bmg9jwrJ7YAA7tRrs4b4NAvfrDKJ2lfl5C9qjFvkozb9wmgpWsNbuhtr/0AK dLqR2rfKlCTuHpaoH+Sjc9mPmHjX8IISjeh18+I8cIINak5jsdSTW8I3ICZhU6laDlcw0rMv SfoRbPn8Oh5+IE9w6ruCvpiAiu3G/PSVcOJ0gK4ookXYfzxbfb+kh4nlWO+HgVJPIk+X8Z8u qSNveXWgmLEnucSeELIl6aRE5Jm4Z2JY9NWFcbsdl9IsDCnWvKwxzcm5EaGcYdolvFZ7emZH zqIUtO6L4Mpao0M1U9rZDh7ODdDLabON4PLhz639taIATgjiT33FsutryLVXDsKZx0zGsPMD yHvsKyT/fFeloNHASEEC9xAA5NVJFzCW7MsR+butAu3X3WZvVefhoTMzRYQyynHKn2hIvbI5 ZjoQhvfdhPrnIrqyNpfkZJ5vzxJLXJbrNQzQHkg+I9Nu2jnNFIFEOUTD8xXQNUc2Cn/z4rxa zzxfXMvQ3e1FyhNdRLnps/vREGDD+gJIc30PSEt41jSUSqtGYecG/F0w0+MOZutlufLl4lL6 O3y+0Ec+jC3z45sTOBV7ef9nPtq1vrBgH8E5CgRVuTsVg0GD+xiOGNJRWJwue7vSqkhV3kn4 UA+XiZZXEyrQFW3HMp9E5KQMA9Mpyvhll3Ecg/WqOsyeOynIClow+a5Jv3+wrQYKskGOdbig J8xq3Sluwir55DYhUflVx/FT0O55TJn0/VW9JPeeDA=
Ironport-hdrordr: A9a23:3jSN8apBppvv+7qe2KAT9AcaV5opeYIsimQD101hICG9E/bo8v xG+c5x6faaslYssR0b9uxoW5PwI080l6QFgrX5VI3KNGOKhILCFuBfBOXZrQEJK0fFmtK0Ws pbAsxD4QLLfD9HZReT2njfL+od
Ironport-phdr: A9a23:fk0AJhdGuQr+jSIAhnQsKoaRlGM+dNTLVj580XLHo4xHfqnrxZn+J kuXvawr0ASTG92DoKsf0rKL+4nbGkU+or+580o+OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF 95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwbL1sI BmssQndqsYajZZsJ6os1hfEomZDdvhLy29vOV+ckBHw69uq8pJk7ypepe8q+dRaUaX9caQ4T LhYAyojPmso+sDltgTNQBWW6HcEXWoYjhRHAw7e7BHnRZjxqTf1tvB82CaBI8L7S60/VCm44 KdqTB/ojzoHNyI8/WrKhMF8kL5XrRS8rBN434PZbp2ZOOdncq/BYN8RWG5NUttRWiBEBI63c okBAPcbPetAr4fzuUYAoxW9CwajGOzi0SNIimPs0KEmz+gtDR3K0Qo9FNwOqnTUq9D1Ob8VX ++v0KnI0SjIYfZM1jfg5ojIdwouofeKXbltdsfRylMgFx7LjlWVs4PlOTWV2/8RvGiA9eZgS P6vhHAoqg5ruTij3NkjhZTUho8MzF3P6Cp2zpovK9KiVE57fcCrEIFWtyyCK4d4Qt8uTmJnt iom1LALu5q2cSkFxpk5xhPSdv+KfpaL7x/hUOucIDd2iXZ7db+8iRi/70utxvHhWsS0zFpHr yxImcTCuHAK0hzc8MmHSv1l80e8xTaAyQ/S5ftfIUwui6XUNoMhzqYqlpUNvkTDECj2mUrsg KCKcUUk/+6l4PnkbLX+vpKQKpF4hwLkPqktlMGzG/k0PwYKUmSB5OiwyaHv8VXkTLlUjfA6i KrUvZ7AKcgGuKK1HxVZ3pss5hqjCTqtzcoVnX0aLFJeZBKIkZLpNUzPIPH5E/iym0ignTF2z P7cJLLhGI/CLn3bnbfhY7l970lcxRI1zd9B6ZNUD6sOIPTpVkDtr9zUFAI5MxCqzOfoEtp9z ZkSVnySDa+EKK/SsFmI6fwzI+SUeYMZpjXwJ+Im6vPgl3M1hFEQcK2z0ZcKdXy0AuxqI0CDb nrthtcBH30Kvg07TOHyi12NSyNTZ3i3X60m4DE7DpmrApvYRoy3nbyBwDm0H5JMaWBdEFyDD 2rnd5icV/cKcy2dOtVhnSAcVbi9V48h0gmjuBLix7p9MuXU4jEYtY7k1NVt++LTkggy+SVoA MSZzmGCVHp5nngIRj8zxKBwu1ZxylaF0ahigvxXD8Zf5/1TUlRyCZmJzOVnBdX7XATpdczPV UqrUty9Rzw9U4Ef2dgLNmN0B8nqrRne0S+jBbldw7+CGZIx+6Ta93PqYdthxmbPz+8sg0RwE ZgHDnGvmqMqr1ubPIXOiUjMzvvCncU02SfM8D3G1m+SpARCVwU2V6zZXHcZb0+QrNLj50qEQ aX9Qa8/PF5nzsiPYrBPdsWvlU9PEfTqJdrbamS3s2yrQwuUy6OFd8znd3hOlD7FBh08mhsIt W2DKRB4Ay6gp2zECzk7FlvybUbl9+9Wo2j9U1M53wiRKUBtyun94QYb0MSVUOhbxbcYoGEhp jFzSU66xM7TAsGcqhBJeqhDZNo7plxck3/Fuhx0JdqtI70Kakc2VQNxsguu0hx2Dt8Fis02t DYwywE0L6uE0VRHfjfe3JbqO7SRJHOgtBaoI7Xb3F3TyrP0su8G9eg4plP/vQqoCltq8nNp1 MNQ2med4ZOCBRQbUJb4WEI6vxZgoLSSbi447oLSnXpiVMv8+jzLxtwsDe0j4h27OcpDPbOND 0n/H9BbT8miJeo2mkS4OwoeNbM3luZ8NMenev2ana+zab86zHT21iIeu9E7ixvUpE8eAqbS0 p0Iwu+VxF6CXjb41hK6t9zv3JpDbncUF3a+zi7tAMhQYLdzdMAFEzTLQYX/y9NgiprqQ3Md+ kSkAgZM28a0dx+baVrV1hYWyFgasXW83ya00nYn9lNh5rraxyHIz+n4IVAEM3NFQWBki3/nO s6pk90KVVPuYgQ03kjAhw6y1+1Qo6JxKHPWSEFDcn3tLm1sZaC3s6KLf89F7J5AXTx/aO2ne hjaT7f8p0FfyCb/By5Ewzt9cTi2u5L/lhg8iWSHLX81omCLMc13wB7e4pTbS5szlnIFTTR2j DDRAHC3JJ+04diEnoyFv+yjH26sTZxcdyD3wJjI7XHroz0xR0Tkzrbqw4WvGBNyySLh0th2S SjEyXS0KpLm0ai3K6Mvf0VlAkP999svH4h/loUqg5RDkXMeh5iT4T8GiTKqa4Udifm4NSFcA 2dSm42wgkCtwkBoI3OXypisU3ycxpEkfNymeiYM3Sl76clWCaCS5bgCnC1vo1P+oxiCBJo11 job1/Yq72YXxu8Tvw94hCaUH74XFE9eFSf30QmU4sC3t+NaaHvlIt3SnAJu2MusCr2PuFQWW 3/kdJIrGylY5d45LU7BwHTorIzoZZODCLBb/g3RmBDGge9PLZs3nfdfnitrN1X2ung9wvI6h xhjjtmq+ZKKIGJ38OelEwZVY3frMtgL9Gin3sM81o6GmpqiFZJ7FnAXUYv0GLi2RSkKu62vN h7SQmRm+jHLQvyGRl7ZsR8+53PXT8LybSHRdCJflI4zAkDEfCk9yEgVRGlox8RpUFDxgpKxN h4iv3gQ4FX8txdBmNVzLxe5V27eoEG1djokQYPZIRZLphdL40OfWSCHxtp6BDoQvpiorQjXb 3eeexwNF2YCHEqNG1HkOLCqo9jG6emRQOSkfbPCZrCHqOoWUPntp9rnyox94zOFLdmCJFFkA uI+00wFVms/BtjUizwUDSEbimrBYtWaqxG15iBs5pnloLK7A0S2vtrJUuIKedx0nnL+yb+OL euRmDp0JX5D25UAyGWJgLkT0VgOij1/IjmgFbNT/SXJTa/WhupWF0tCMXM1ZJAOtvltmFAUY Z2+6Ju9zLNzg/8rBk0QUFXgnpvsfskWOySnM1iBAk+XNbOALDmNwsftYKr6R6cD6Ycc/xC2p zufFFfuezqZkDy8HROmLO9JhSedFBdF/pyhfwZkEi7uQM+sOXjZeJdnyCY7x7E5nCaALWkHL T11aF9AtJWW4Dxdi/M5EHcH82ZoPeCf3SuV8qOLT/Re+esuCSNymeVA5X08wLYA9yBISst+n y7Kp8JvqVWrwaGfjyBqWx1UpnNXlZqG6A98bL7B+MAKChOmtFodqH+dABMQq555B83z7upOn 8PXmvu7IX8H+tbQt6P06ODfM4SaLHcxOAGvFTLJXlJtpd+DM2zAgkVb1vqJsGCJo4gzsd7hl IdcE9ezsXQ+DbUHFkl1FcdELZtqDGtMrA==
Ironport-sdr: 67d43cb6_/0qWtx1wemLU8TgcKQ6Xr5PqAXEns6slwAV9J6YQZQ2dd// TT3+UI5jlpRBYpQQ1rvog87vtJgaTPZDfeX0JTQ==

*** CALL FOR PARTICIPATION ***

*Apologies for multiple postings*

ACL2-2025

19th International Workshop on the ACL2 Theorem Prover and Its
Applications

May 12-13, 2025, Austin, Texas, USA and also online

http://www.cs.utexas.edu/users/moore/acl2/workshop-2025/index.html

The 2025 ACL2 Workshop will be held in Austin, Texas, USA and online.
We invite users of ACL2, users of other theorem provers, and persons
interested in the applications of theorem proving technology to
attend. An invited keynote talk will be given by Swarat Chaudhuri
(University of Texas at Austin), "Scaling Formal Verification with
Machine Learning"; a second invited keynote talk is anticipated. See
the above website for accepted papers as well as updates, which will
include a program with details on a pre-workshop reception on May 11
and a banquet on May 12.

REGISTRATION

Registration details may be found at:

https://acl2.regfox.com/acl2-workshop-2025

Note that discounted fees for early registration end after March 31.

AIMS AND SCOPE (quoting from
https://www.cs.utexas.edu/users/moore/acl2/workshop-2025/index.html#scope):

The ACL2 Workshop series is the major technical forum for users of the
ACL2 theorem proving system to present research related to the ACL2
theorem prover and its applications. ACL2 is an industrial-strength
automated reasoning system, the latest in the Boyer-Moore family of
theorem provers. The 2005 ACM Software System Award was awarded to
Boyer, Kaufmann, and Moore for their work on ACL2 and the other
theorem provers in the Boyer-Moore family.

ACL2-2025 will be held in Austin, Texas, USA and also online, May
12-13, 2025. The workshop will take place in person on the University
of Texas at Austin campus. In addition to in-person participation,
the workshop will support online participation for all talks and
presentations. The workshop will be the 19th in the series of ACL2
workshops, which occur approximately every 18 months. It will feature
technical papers as well as rump sessions that discuss ongoing
research.

FOR MORE INFORMATION:

See the website
https://www.cs.utexas.edu/users/moore/acl2/workshop-2025/index.html
for further information including accepted papers, organization,
venue, and lodging.

[Coq-Club] ACL2-2025 Call for Participation, Matt Kaufmann, 03/14/2025