coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] ACL2-2025 Second Call for Participation

From: Matt Kaufmann <kaufmann AT cs.utexas.edu>
To: kaufmann AT cs.utexas.edu
Subject: [Coq-Club] ACL2-2025 Second Call for Participation
Date: Mon, 14 Apr 2025 10:23:19 -0500
Authentication-results: mail3-smtp-sop.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:d7Mr2qsW88+AJpepnoPwh1VJy+fnVNpaMUV32f8akzHdYApBsoF/q tZmKTzQPa6KMzH1KN0laIrlpBlX75aExtYyHApvrSo8EH4QgMeUXt7xwmXYb3rDdJWbJK5Ex 5xDMYeYdJhcolv0/ErF3m3J9CEkvU2wbuOgTrSCYEidfCc8IA85kxVvhuUltYBhhNm9Emult Mj7yyHlEAbNNwVcbCRNtspvlDs15K6v4G9B4gRnDRx2lAa2e0c9XMp3yZ6ZdCOQrrl8RoaSW +vFxbelyWLVlz9F5gSNz94X2mVTKlLjFVDmZkh+A8BOsTAezsAG6ZvXAdJHAathZ5plqPgqo DlFncTYpQ7EpcQgksxFO/VTO3kW0aGrZNYriJVw2CCe5xSuTpfi/xlhJH0fD4AZ3sR5PWhl1 /pGLWgHZzHZrsvjldpXSsE07igiBM/mI4YWvDdr1nfEEfs2SIuFTqnXjTNa9G5q1oYeRrCHP JtfMGM3BPjDS0Un1lM/C5sjkuKhgH/XeCYetU6YtaMspWXf0WSd1ZC0aYaPJoXUFJQ9ckCwq 0yX/HrFGTcgEdm462rU7Sym2sTNpHauMG4VPOHnq6Ez6LGJ/UQYDwRTXl+mq9Gim0umUpReL VYV82wgt8APGFeDSNTiWhS+5nWf+AMAVspZCKs35BzlJrfoDxixOkE2Qz9lStIaveQUQ2Ivj lWAvonALGk62FGKck61+rCRpDK0HCEaK24eeCMJJTfpBfG/+unfaTqTH75e/L6JszHjJd3nL 9m3QMUWgbgMiMcNka6gu03bjiKlvd7EQhNdCuTrsoCNs10RiG2NPtLABb3nARBodtbxor6p5 idspiRmxLpSZaxhbQTUKAn3IJmn5uyeLBrXikN1Ep8q+lyFoiH/Id0OsWgmfBg2aK7onAMFh meP4Wu9A7cPYxOXgVNfPepd9uxwk/O5S4SNug78NYoTMvCdizNrDAkyOhPPhggBYWAxl6AhN I2AcNq9RXEUQbhq3DOtD+4BmbY23Tw/wwvuqWPTlHyaPU6lTCfNE98taQLeBshntv/snekg2 48PXyd840wPCLWmCsQWmKZPRW03wY8TXMGt85wNLrfTfmKL2ggJUpfs/F/oQKQ994w9qwsC1 ijVtpZwkQKn2y/0Ok+RZ2p9abjie596oDhpdWYvJFukkTxrK4qm8K5VJdN9cKgF5d5T66d+b 8AEXMGcXdVJaDDMoAoGYbfH8YdNSRWMhCC1BRSDXgQRRZBbajLsxs7FZSrqrSkHMTq2v5Axo pqmzQLqfqAATAVDUufTNfajlQqxt3lAmuljAhLEDecPSXXJ7bpVEXXQj+A2Ee4IOx7s1juX7 CfIIBY69M3mgZ45z8nNvo+A97yWKupZGlFIOkXm9pC0Pjn+0kv65qEYS8eOXzTWdF2syZWYf e8Pks3NaqwWrmhFo69XMuhNz5tnw/DNurUD7ABvPEuTXmSRErk6f0W3h5hehJZsmI1clxC9A H+U299gPr6MBsPpPXgRKCchbcWBzfskoSbT39tkPHTF4DJLw5TfXXVwJxWsjAlvHIlxOq4hw sYjv5cywC67gRwILN2Hr35180KhE38+aJgk56oqWNLTtgkWy195ccP9DA3y68qxcNliCBQhD QKVo6vgvI5i4HT+XUA9LlX35toFt68y4EhL6HQgO2W2nsH0g65r/R9JrhUyYAdn7jRG9ONRO GN6ahR5CpvSzgdNmfp8ZTmNGh5ANjKd6Efe21sEr0yHbkiKB0jmDnwxBvaJx28dq1ljRzl8+ KrC7nTIShPoQZ3V8g4tf3A9sN3lb9h61jOaqfCdB87fQqULO2v0sJGhdU8jikXBA/pooGblu OMz3uJ7SZOjBB4qu6dhVrWrj+UBeiulel5Hb+pqpp4SPGfmfzq35ziCBmaxdu5JJN3I6UWIM NNvFO0eSyWB0DuykR5DCZ4uO7NUmNsb1OgGcJ7vJk8EtOK7hRhtu5Ty6CP/pTEKR/NDrMUDE b7SJgmySjGouXhpmmH2vJZlPEi8aoI6fwHS5r2+39gIMJMhi9tSV38O/IG6hUjIDzs/zSmo5 FvCQ4T0091dzZ9dmtqwM6dbWCSxB9DBdMWJ1wGRsd9fMIrDHvmShjMwt2vYBV13PKQQaftzh 7+ioN7652KbnbcUAkTyuYiNKLlN3uq2BNFoC8PQKGIAuzmvQ+ru3kcn10WnD6IRi/JbxM2sZ zXgWfuKbdRPButsnixEWRZRAzM2KvrRbJ65gQifsv7VKBwW8TKfHeOd7XWzMF1qLH4ZCabfV D3xle2lvO1DjYJ2AxQBOfFqLrl4LHLnWookb9fBjiaZPEb5nmK9vqbeqjR45QHpEnWkFOPI0 aDBTDX6dzWwv/js5/NduIpQoBYWLShchc8dQ0EjwON12guKVDM+EecgMJs4U8Ae1mS40Zzjf zjCYVczESi3D3wObRz458+lRQuFQPAHPtDiPDEy4keIcGGMCZidBKd6vDJVi5usluAPEMn8Q T3fxpHxAvR16pdkWuMa4LqwmqF62v7Kz2lO9Ezg+yA3KwhLGq0EjRSNAyIUPREr0emU/KkIG YTxbWtfBlynRF74CoBtd2M99NQxomb01ztxBcuQ6I+3hmhYpdGsDNX0IKfuzrATZd9MKbITL Z8yq61h/EjOskEuVWAVVx7FTEO65T9n3iR3EUM7eTAvog==
Ironport-hdrordr: A9a23:Ik6xBKv8vmZz5vQZ398om74j7skDdNV00zEX/kB9WHVpm62j5q WTdZEgviMc5wxwZJhNo7+90cq7MBHhHPxOkOos1N6ZNWGN1VdAR7sC0WKN+VPd8x2VzIJgPS gMSdkbNDQuNykcsS4qiDPIdeod/A==
Ironport-phdr: A9a23:bNHs+hT13J/6X3bLpC07UKgcbtpsonqVAWYlg6HPa5pwe6iut67vI FbYra00ygOSB8ODs7ke0bKG4ujJYi8p39WoiDM4TNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB 89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCybL58M hm6txndutUZjYd8NKo91hjEr39VcOlK2G1kIk6ekBn76sqs5pBv9Dhetew8/MBaS6X6eKo4T b1cDDs4Nm0++dPmuxreQwaR/3UQSmoZnAZGDAjD9xH6Q4z+sjDmuepn2SmVJtP5QLYpUjm/9 ahrSRvoiCAaNz4l9Wzcl8J9gL5HrB+nuhdwxJLZbY+JOPZjZ6/RYc4WTndFUspMVyFNB4WxZ JYNAeUcJ+ZVt4nzqUUToxWwBgejC//gxyRUhnPqx6A2z/gtHR3a0AEmAtkAsG7UrNLwNKoKV u661rXIzSneZP1Twzj99YbIchU7rvGKW7J7bM3cyUo1GAPYgFWQrJbqPzWT1ukWr2eb9PBsV f+zi2E5pAB+uCOvyt0yhYbUm4IY01bJ/jh2z4gpP9O3UlJ7YcK6H5tKsSGXL5d6TMM+T2xrt yg21qMLtJy/cSULx5oq2R/SZuGEfoWW4R/uVuKcLDZ4in9hZr+yhBi8/Fajx+HgS8W50EpGo ytDn9LRuH4N0BnT5dKGSvt75kqhxCqP2B7c6+5eOkA4j7TUJIM8wrIojJocr0vDHiHxmET5l qOZakIk+u2u5u/6YbvmvoeRO5Jqhgz9KKgjmcKyDf4lPgUAW2WX4/mw2KD/8UHhXblGkP47n rPavZ3UP8gXu7C1DxNP3oo+5BuzEzGr28kGkHkDMVJFYw6HgJbzO1/TIfD5DOmwjkywnDpt2 vvIJKfuAo/XIXjGiLrhfahy60pbyAcry9BQ+ZxVCrQbL/L1QEP+qMfYAgUkMwyo3enmB89y1 pgEVW2RH6CZLbvesV6O5u0xP+mBfJIZtCj+JvQ/5PPjg2U1lUITcKStx5cbdW20Euh+L0Wce 3Xsg9MBEWkQvgo5SeznkF6CXiROZ3a8WqIz/Dc7CIS9AIjfXYChmqGB3DulEZxZfG9GEUqAH mn1eIWZQ/sMbjmdLdd7kjMYTbihV5Mh1Ra2uQPn07ZnNPbb+jUEtZL/09h4//HclRYr9TBtE 8ud13yNQHpvk2MTRz422bh/rlZnxleC16h4mf1YGsZJ6/NHSAdpfaLbmu9zFt73UwTHVtySD ku6T8WvGnc8Qs9i7cUJZhNYEsm+xjPKwiSvCrkT3+iIDYE696va2VD6PIBg13vW3bJnglU7F JgcfVa6j7JyolCAT7XClF+Uwv/3HUx99CvE9WPYiHGLoFkdSwloF6PMQXEYYELS69X//ELLC bG0Wvw8KgUU78mEJ+NRb8Hxy01cTaLgMcnQZmu3nU+7HlCV2r6cZZGsdmkAj23GEEZRqwkI5 j6dMBQmQCKoombQFjtrQFHmfk3p+O94gHigCFIowhGDdAts26fmsgUNi6mkQugIlqkBpD9nq zhwGwOl2MnKDtObuwd7VKNRftY05hFMziTEqwFtN4fmIqx/7rIHWyJwuU6mlxB+C4Eb1NMvs Gtv1w1qb6SRzFJGcTqcm5H2ILzebGforlipbObN11fS3czzmO9H4ekkq1jloACiF1Yzu3Rh3 d5P1nKA55LMRAMMWJP1W0wz+lB0vbbfKiU64orV0zVrP8zW+nfB0s8nAeIjzD6rZJFCLK6UH RS0HsEHRoCvJOEsh1m1f0ccJukBkcx8d8iidvaAxOuqJLM5xmLg3T8BudsslBvVr3kZKKaAx ZsOzvCG0xHSUj79iAzkqcXrgcVfYilUGGOjyC/iDYoXZ6tofI9NB339Rq//jth4mZPpXGZVs VC5AFZTksygZBSXZlr79QZLk1kLrGyugm21wyE+wFRL5uKPmTfDxejvbk9NOWdWSmxri1HEK pPykswXTEGzKQUliVH2gCSyj7ger6N5IW7JRE5OdCWjNGBuXJy7sb+aatJO4pcl2clOeNy1e kvSCrv0oh9BljjmA3Mb3zcjMTejppT+mRV+zmObNnd66nTDK4l8whLW5dqUQvA0vHJORyBlh zzeAF6UNMLv4MmZh57Y9O2ySiqtW4ZSfi/i0Y6b/HLhtSs6WlvmxKH1w4S/WQEhmTf2zdxrS TnFoHOeKsHw2qK2PPgmNkhkCVng6tZrT4R3k48+npYVijARgpSY+2ZCkH+maI8Ln/KlKiNWF HhSmoaGhWqtkFduJX+I2Y/jA3CUw886IsK/fntTwSUlqcZDFKaT6rVA2ypzuFux6wzLMp0f1 n8Qz+Uj7HkCjqQHog0om2+eC60cGEBeOwTnjFKV892upb4RaWqyO+vVtgI2jZW6AbeOrxsJE nXwZ5knFCl2xs5kdk/Q3W368cfpdMSaPrdx/lWE1hzHieZSMpc4kPEH0DFmNWzKtnog0+cnj BZq0MLyrM2dJm5q5q78Hg9AO2i/eZYI4j+0x/U7/I7ez8W1E55mADlOQJb4UafiDmcJrfq+f weWTG9l8CfdSeGZRFTOrh4+9zrOC8z5bivHYilCi4w5FV/EfRQ64khcXS1mzMdjRkb6n4q/I AEgvWlZ51jzrgZAx7BfLAHxFGLWpQPudys5WJGEahda80lU7kPRe6Ry98pLFjpDtt2kpQ2Jc SmAYhhQSHoOQgqCDkziOb+n4Z/B9fKZD6ywNamGbbKLoO1YH/CGoPDnmpNh5CqJP96TM2NKC fAk30NFG3tiXdnFliUGUGoamz+FY8OApRi68zF6tYjmqqStCFmpvNDeTeILaZ1m4HXUye+bO vSVhTplJDoQzZ4KyXLSifAe0FMUlyByZmytHLAH5mbGSKPdnLMSDgZOMnkjcpsTqftnj08UY JaI77G9nqR1hfM0FVpfAFnom8XyINcPP3n4L1TfQkCCKLWBIzTPhcDxe6K1D7NK34A2/1W9v yiWF0j7M3GNjT7sAlqsOPxCiSidOjRVo8egbht9AHOlQd77IE7eUpc/nXgtzLs4i2mff3YbK iR5elhRo6e46y5Hh/x5XWdaqGd5IPmNgGCU4/SSefN0+bN7Ry9zkexd+nEzzbBYuTpFSPJCk yzXttdyoluin7rH2n99XRFJsDoOmJOTsBAoJ/DC7pcZEyWhnlpF/SCKBh8NvdcgFtD/p/Ua1 I3UjKyqYD4KttvQ+YF07yf8I9nBLWYsIRPyXjPYEVlcJdZOHWrEwVFBneGb7TuYooVo8vAEe bIIR6BeXVpzHehcF1hoDNUZZpp7Q2F9+YM=
Ironport-sdr: 67fd2882_1hPrtrkDplXpH1cO+uCaXgTNe8UQLd4AocLNxbiD4AkeVWm TTtRmIvYh55pDhrk9vxc6XBA61LB+cdz9PKU9FA==

*** SECOND 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. There will be two invited keynote talks: "Scaling Formal
Verification with Machine Learning" by Swarat Chaudhuri (University of
Texas at Austin), and "The Future of ACL2 Community" by Warren
A. Hunt, Jr. (UT Austin) and Anna Slobodova (Arm Ltd). 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 (including free online-only registration) may be
found at:

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

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 Second Call for Participation, Matt Kaufmann, 04/14/2025